Abstract
Tableau systems are very popular in AI for their simplicity and versatility. In recent papers we showed that tableau-based procedures are intrinsically inefficient, and proposed an alternative approach of building decision procedures on top of SAT decision procedure. We called this approach “SAT-based”. In extensive empirical tests on the case study of modal K, a SAT-based procedure drastically outperformed state-of-the-art tableau-based systems. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logics.
The authors thank Fausto Giunchiglia for providing valuable feedback.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Bresciani, E. Franconi, and S. Tessaris. Implementing and testing expressive Description Logics: a preliminary report. In Proc. International Workshop on Description Logics, Rome, Italy, 1995.
B. F. Chellas. Modal Logic — an Introduction. Cambridge University Press, 1980.
M. D'Agostino and M. Mondadori. The Taming of the Cut. Journal of Logic and Computation, 4(3):285–319, 1994.
M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.
G. DeGiacomo and F. Massacci. Tableaux and Algorithms for Propositional Dynamic Logic with Converse. In Proc. of the 5th International Conference on Principles of Knowledge Representation and Reasoning — KR'96, Cambridge, MA, USA, November 1996.
M. Fitting. Proof Methods for Modal and Intuitionistic Logics. D. Reidel Publishg, 1983.
E. Giunchiglia, F. Giunchiglia, R. Sebastiani, and A. Tacchella. More evaluation of decision procedures for modal logics. In Proc. of the 6th International Conference on Principles of Knowledge Representation and Reasoning — KR'98, Trento, Italy, November 1997.
F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures — the case study of modal K(m). Technical Report 9611-06, IRST, Trento, Italy, 1996.
F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures — the case study of modal K. In Proc. of the 13th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, New Brunswick, NJ, USA, August 1996. Springer Verlag. Also DIST-Technical Report 96-0037 and IRST-Technical Report 9601-02.
F. Giunchiglia and R. Sebastiani. A SAT-based decision procedure for ALC. In Proc. of the 5th International Conference on Principles of Knowledge Representation and Reasoning — KR'96, Cambridge, MA, USA, November 1996. Also DIST-Technical Report 9607-08 and IRST-Technical Report 9601-02.
U. Hustadt and R.A. Schmidt. On evaluating decision procedures for modal logic. In Proc. of the 15th International Joint Conference on Artificial Intelligence, 1997.
R. Sebastiani and D. McAllester. New upper bounds for satisfiability in modal logics — the case-study of modal K. Technical Report 9710-15, IRST, Trento, Italy, October 1997.
R. M. Smullyan. First-Order Logic. Springer-Verlag, NY, 1968.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sebastiani, R., Villafiorita, A. (1998). SAT-based decision procedures for normal modal logics: A theoretical framework. In: Giunchiglia, F. (eds) Artificial Intelligence: Methodology, Systems, and Applications. AIMSA 1998. Lecture Notes in Computer Science, vol 1480. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0057460
Download citation
DOI: https://doi.org/10.1007/BFb0057460
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64993-9
Online ISBN: 978-3-540-49793-6
eBook Packages: Springer Book Archive