|Títol||On the Implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers|
|Publication Type||Conference Paper|
|Year of Publication||2013|
|Authors||Alsinet T, Barroso D, Bejar R, Bou F, Cerami M, Esteva F|
|Conference Name||7th International Conference on Scalable Uncertainty Management, SUM 2013|
|Edition||Weiru Liu, V. S. Subrahmanian and Jef Wijsen|
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.
- Quant a IIIA