Abstract
In the last two decades, modal and description logics have been applied to numerous areas of computer science, including artificial intelligence, formal verification, database theory, and distributed computing. For this reason, the problem of automated reasoning in modal and description logics has been throughly investigated.
In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic K m , and of its notational variant, the description logic \(\ensuremath{\mathcal{ALC}}\). Although simple in structure, K m /\(\ensuremath{\mathcal{ALC}}\) is computationally very hard to reason on, its satisfiability being PSPACE-complete.
In this paper we explore the idea of encoding K m /\(\ensuremath{\mathcal{ALC}}\)-satisfiability into SAT, so that to be handled by state-of-the-art SAT tools. We propose an efficient encoding, and we test it on an extensive set of benchmarks, comparing the approach with the main state-of-the-art tools available.
Although the encoding is necessarily worst-case exponential, from our experiments we notice that, in practice, this approach can handle most or all the problems which are at the reach of the other approaches, with performances which are comparable with, or even better than, those of the current state-of-the-art tools.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Brand, S., Gennari, R., de Rijke, M.: Constraint Programming for Modelling and Solving Modal Satisfability. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, Springer, Heidelberg (2003)
Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. D. Reidel Publishg (1983)
Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, Springer, Heidelberg (1996)
Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K(m). Information and Computation 162(1/2) (2000)
Halpern, J.Y.: The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. AI 75(3), 361–372 (1995)
Halpern, J.Y., Moses, Y.: A guide to the completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence 54(3), 319–379 (1992)
Horrocks, I., Patel-Schneider, P.F.: Optimizing Description Logic Subsumption. Journal of Logic and Computation 9(3), 267–293 (1999)
Hustadt, U., Schmidt, R.A., Weidenbach, C.: MSPASS: Subsumption Testing with SPASS. In: Proc. DL 1999, pp. 136–137 (1999)
Ladner, R.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comp. 6(3), 467–480 (1977)
Massacci, F.: Single Step Tableaux for modal logics: methodology, computations, algorithms. Journal of Automated Reasoning Vol. 24(3) (2000)
Pan, G., Sattler, U., Vardi, M.Y.: BDD-Based Decision Procedures for K. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, Springer, Heidelberg (2002)
Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, Springer, Heidelberg (2003)
Sebastiani, R., Vescovi, M.: Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/\({\mathcal ALC}\). Extended version. Technical Report DIT-06-033, DIT, University of Trento (May 2006), http://www.dit.unitn.it/~rseba/sat06/extended.ps
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sebastiani, R., Vescovi, M. (2006). Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/\(\mathcal{ALC}\) . In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_15
Download citation
DOI: https://doi.org/10.1007/11814948_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37206-6
Online ISBN: 978-3-540-37207-3
eBook Packages: Computer ScienceComputer Science (R0)