@conference {5171,
title = {On the Implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers},
booktitle = {7th International Conference on Scalable Uncertainty Management, SUM 2013},
volume = {8078},
year = {2013},
month = {16/09/2013},
pages = {325-330},
publisher = {Springer},
organization = {Springer},
edition = {Weiru Liu, V. S. Subrahmanian and Jef Wijsen},
abstract = {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.},
url = {http://link.springer.com/chapter/10.1007\%2F978-3-642-40381-1_25},
author = {Teresa Alsinet and David Barroso and Ramon Bejar and F{\`e}lix Bou and Marco Cerami and Francesc Esteva}
}