Abstract
We explore to what extent and how efficiently constraint programming can be used in the context of automated reasoning for modal logics. We encode modal satisfiability problems as constraint satisfaction problems with non-boolean domains, together with suitable constraints. Experiments show that the approach is very promising.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Areces, C., Gennari, R., Heguiabehere, J., de Rijke, M.: Tree-based Heuristics in Modal Theorem Proving. In: Proc. ECAI 2000, pp. 199–203. IOS Press, Amsterdam (2000)
Blackburn, P., De Rijke, M.: Zooming in, zooming out. Journal of Logic, Language and Information 6, 5–31 (1997)
Blackburn, P., De Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)
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), 158–178 (2000)
Haarslev, V., Möller, R.: RACER (September 2002), http://kogs-www.informatik.uni-hamburg.de/~race/
Heuerding, A., Schwendimann, S.: A Benchmark Method for the Propositional Modal Logics K, KT, S4. Technical Report IAM-96-015, University of Bern (1996)
Horrocks, I.: FaCT (September 2002), http://www.cs.man.ac.uk/~horrocks/FaCT/
Horrocks, I., Patel-Schneider, P.F., Sebastiani, R.: An Analysis of Empirical Testing for Modal Decision Procedures. Logic J. of the IGPL 8(3), 293–323 (2000)
MSPASS V 1.0.0t.1.2.a. February 23 (2001), URL: http://www.cs.man.ac.uk/~schmidt/mspass
Pan, G., Sattler, U., Vardi, M.Y.: BDD-Based Decision Procedures for K. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 16–30. Springer, Heidelberg (2002)
Patel-Schneider, P.F.: DLP (September 2002), URL: http://www.bell-labs.com.user/pfps/dlp/
Tacchella, A.: ∗ SAT System Description. In: Collected Papers from the International Description Logics Workshop 1999, CEUR (1999)
TANCS: Tableaux Non-Classical Systems Comparison, January 17 (2000), URL: http://www.dis.uniroma1.it/~tancs
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brand, S., Gennari, R., de Rijke, M. (2003). Constraint Programming for Modelling and Solving Modal Satisfiability. In: Rossi, F. (eds) Principles and Practice of Constraint Programming – CP 2003. CP 2003. Lecture Notes in Computer Science, vol 2833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45193-8_55
Download citation
DOI: https://doi.org/10.1007/978-3-540-45193-8_55
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20202-8
Online ISBN: 978-3-540-45193-8
eBook Packages: Springer Book Archive