Abstract
The modal satisfiability problem is solved either by using a specifically designed algorithm, or by translating the modal logic formula into an instance of a different class of problem, such as a first-order logic problem, a propositional satisfiability problem, or, more recently, a constraint satisfaction problem. In the latter approach, the modal formula is translated into layered propositional formulae. Each layer is translated into a constraint satisfaction problem which is solved using a constraint solver. We extend this approach to the modal logics KT and S4 and introduce a range of optimizations of the basic prototype. The results compare favorably with those of other solvers, and support the adoption of constraint programming as implementation platform for modal and other related satisfiability solvers.
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
Horrocks, I.: The FaCT System. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 307–312. Springer, Heidelberg (1998)
Patel-Schneider, P.F.: DLP system description. In: Proceedings of the 1998 International Workshop on Description Logics Workshop (DL 1998), vol. 11, pp. 87–89 (1998), CEUR-WS.org
Ohlbach, H., Nonnengart, A., de Rijke, M., Gabbay, D.: Encoding two-valued non-classical logics in classical logic. In: Handbook of Automated Reasoning, pp. 1403–1486. Elsevier Science, Amsterdam (2001)
Giunchiglia, F., Sebastiani, R.: Building Decision Procedures for Modal Logics from Propositional Decision Procedure. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 583–597. Springer, Heidelberg (1996)
Brand, S., Gennari, R., de Rijke, M.: Constraint programming for modelling and solving modal satisfiability. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 795–800. Springer, Heidelberg (2003)
Brand, S., Gennari, R., de Rijke, M.: Constraint methods for modal satisfiability. In: Apt, K.R., Fages, F., Rossi, F., Szeredi, P., Váncza, J. (eds.) CSCLP 2003. LNCS (LNAI), vol. 3010, pp. 66–86. Springer, Heidelberg (2004)
Wallace, M.G., Novello, S., Schimpf, J.: ECLiPSe: A platform for constraint logic programming. ICL Systems Journal 12(1), 159–200 (1997)
Horrocks, I., Patel-Schneider, P.: FaCT and DLP. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 27–30. Springer, Heidelberg (1998)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)
Stevenson, L.: Modal Satisfiability in a Constraint Logic Environment. University of South Africa, M.Sc dissertation (2008)
Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. Journal of Automated Reasoning 24(3), 297–317 (2000)
Jaeger, G., Balsiger, P., Heuerding, A., Schwendimann, S.: K, KT, S4 test data sets (retrieved, September 2007), http://www.iam.unibe.ch/~lwb/benchmarks/benchmarks.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stevenson, L., Britz, K., Hörne, T. (2008). KT and S4 Satisfiability in a Constraint Logic Environment. In: Ho, TB., Zhou, ZH. (eds) PRICAI 2008: Trends in Artificial Intelligence. PRICAI 2008. Lecture Notes in Computer Science(), vol 5351. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89197-0_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-89197-0_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89196-3
Online ISBN: 978-3-540-89197-0
eBook Packages: Computer ScienceComputer Science (R0)