2020-02-22T11:45:24Z
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.
Research partially funded by the Spanish MICINN projects ARINF (TIN2009-14704-C03-01/03) and TASSAT (TIN2010-20967-C04-01/03), MINECO project EdeTRI (TIN2012-39348-C02-01), Agreement Techologies (CONSOLIDER CSD 2007- 0022), Catalan Government (2009SGR-1433/34) and ESF project POST - UP II No. CZ.1.07/2.3.00/30.0041 that is co-financed by the European Social Fund and the state budget of the Czech Republic.
Peer Reviewed
2016-06-27T17:40:45Z
2016-06-27T17:40:45Z
2013
2016-06-27T17:40:45Z
comunicación de congreso
doi: 10.1007/978-3-642-40381-1_25
issn: 0302-9743
isbn: 978-3-642-40380-4
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