2020-01-25T05:23:12Z
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
On the implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers
Alsinet, Teresa
Barroso, David
Bejar, Ramon
Bou, Felix
Cerami, Marco
Esteva, Francesc
Ministerio de Economía y Competitividad (España)
Generalitat de Catalunya
Description logics
Fuzzy product logic
SMT solvers
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.
2016-06-27T17:40:45Z
2016-06-27T17:40:45Z
2013
2016-06-27T17:40:45Z
comunicación de congreso
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
eng
Postprint
Sí
openAccess
Springer