2019-11-20T18:05:10Z
http://digital.csic.es/dspace-oai/request
oai:digital.csic.es:10261/134120
2018-08-09T10:11:14Z
com_10261_60
com_10261_4
col_10261_1195
Alsinet, Teresa
Barroso, David
Bejar, Ramon
Bou, Felix
Cerami, Marco
Esteva, Francesc
2016-06-27T17:40:45Z
2016-06-27T17:40:45Z
2013
Lecture Notes in Artificial Intelligence 8078. Scalable Uncertainty Management, 7th International Conference, SUM 2013 Washington, DC, USA, September 16-18, 2013, Proceedings, pp 325-330.
http://hdl.handle.net/10261/134120
10.1007/978-3-642-40381-1_25
http://dx.doi.org/10.13039/501100003329
http://dx.doi.org/10.13039/501100002809
In this paper we explain the design and preliminary implementation of a solver for the positive satisfiability problem of concepts in a fuzzy description logic over the infinite-valued product logic. This very solver also answers 1-satisfiability in quasi-witnessed models. The solver works by first performing a direct reduction of the problem to a satisfiability problem of a quantifier free boolean formula with non-linear real arithmetic properties, and secondly solves the resulting formula with an SMT solver. We show that the satisfiability problem for such formulas is still a very challenging problem for even the most advanced SMT solvers, and so it represents an interesting problem for the community working on the theory and practice of SMT solvers.
eng
openAccess
Description logics
Fuzzy product logic
SMT solvers
On the implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers
comunicaciĆ³n de congreso