TitleOn the Implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers
Publication TypeConference Paper
Year of Publication2013
AuthorsAlsinet T, Barroso D, Bejar R, Bou F, Cerami M, Esteva F
Conference Name7th International Conference on Scalable Uncertainty Management, SUM 2013
EditionWeiru Liu, V. S. Subrahmanian and Jef Wijsen
Date Published16/09/2013

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.