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.
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F.: Tableau algorithms for description logics. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 1–18. Springer, Heidelberg (2000)
Cerami, M., Esteva, F., Bou, F.: Decidability of a description logic over infinite-valued product logic. In: Proceedings of KR 2010 (2010)
Cerami, M., Straccia, U.: On the (un)decidability of fuzzy description logics under łukasiewicz t-norm. Information Sciences 227, 1–21 (2013)
Cignoli, R., Torrens, A.: An algebraic analysis of product logic. Multiple-Valued Logic 5, 45–65 (2000)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Haarslev, V., Sebastiani, R., Vescovi, M.: Automated Reasoning in \(\mathcal{ALCQ}\) via SMT. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 283–298. Springer, Heidelberg (2011)
Hájek, P.: Making fuzzy description logic more general. Fuzzy Sets and Systems 154(1), 1–15 (2005)
Hustadt, U., Motik, B., Sattler, U.: Reducing SHIQ-description logic to disjunctive Datalog programs. In: Proceedings of KR 2004, pp. 152–162 (2004)
Straccia, U., Bobillo, F.: Mixed integer programming, general concept inclusions and fuzzy description logics. In: Proceedings of EUSFLAT 2007, pp. 213–220 (2007)
Vidal, A., Bou, F., Godo, L.: An SMT-based solver for continuous t-norm based logics. In: Hüllermeier, E., Link, S., Fober, T., Seeger, B. (eds.) SUM 2012. LNCS, vol. 7520, pp. 633–640. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alsinet, T., Barroso, D., Béjar, R., Bou, F., Cerami, M., Esteva, F. (2013). On the Implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers. In: Liu, W., Subrahmanian, V.S., Wijsen, J. (eds) Scalable Uncertainty Management. SUM 2013. Lecture Notes in Computer Science(), vol 8078. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40381-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-40381-1_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40380-4
Online ISBN: 978-3-642-40381-1
eBook Packages: Computer ScienceComputer Science (R0)