×

Building decision procedures for modal logics from propositional decision procedures – the case study of modal K. (English) Zbl 1415.03022

McRobbie, M. A. (ed.) et al., Automated deduction – CADE-13. 13th international conference on automated deduction, New Brunswick, NJ, USA, July/August 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1104, 583-597 (1996).
Summary: The goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we describe an algorithm, based on an implementation of the Davis-Putnam-Longemann-Loveland procedure, which tests satisfiability in modal K. The algorithm is compared with a tableau based decision procedure. The experimental results show that our algorithm outperforms this system. The testing is performed following a newly developed methodology which, among other things, allows us to classify problems according to an easy to hard pattern.
For the entire collection see [Zbl 1102.68317].

MSC:

03B35 Mechanization of proofs and logical operations
03B25 Decidability of theories and sets of sentences
03B45 Modal logic (including the logic of norms)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

TPTP
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] A. Armando and E. Giunchiglia. Embedding Complex Decision Procedures inside an Interactive Theorem Prover. Annals of Mathematics and Artificial Intelligence, 8(3-4):475-502, 1993. · Zbl 1034.68541 · doi:10.1007/BF01530803
[2] M. Buro and H. Buning. Report on a SAT competition. Technical Report 110, University of Paderborn, Germany, November 1992. · Zbl 1023.68656
[3] R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, September 1992. · doi:10.1145/136035.136043
[4] M. D’Agostino. Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information, 1:235-252, 1992.
[5] M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.
[6] M. D’Agostino and M. Mondadori. The Taming of the Cut. Journal of Logic and Computation, 4(3):285-319, 1994. · Zbl 0806.03037
[7] M. Fitting. First-Order Modal Tableaux. Journal of Automated Reasoning, 4:191-213, 1988. · Zbl 0648.03004 · doi:10.1007/BF00244394
[8] M. L. Ginsberg. Dynamic Backtracking. Journal of Artificial Intelligence Research, 1:25-46, 1993. · Zbl 0900.68179
[9] F. Giunchiglia and L. Serafini. Multilanguage hierarchical logics (or: how we can do without modal logics). Artificial Intelligence, 65:29-70, 1994. · Zbl 0787.68093 · doi:10.1016/0004-3702(94)90037-X
[10] F. Giunchiglia, L. Serafini, E. Giunchiglia, and M. Frixione. NonOmniscient Belief as Context-Based Reasoning. In Proc. IJCAI13, pages 548-554, 1993.
[11] J.Y. Halpern and Y. Moses. A guide to the completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54(3):319-379, 1992. · Zbl 0762.68029 · doi:10.1016/0004-3702(92)90049-4
[12] B. Hollunder, W. Nutt, and M. Schmidt-Schauß. Subsumption Algorithms for Concept Description Languages. In Proc. ECAI8, pages 348-353, 1990.
[13] F. Massacci. Strongly analytic tableaux for normal modal logics. In Proc. CADE12, 1994. · Zbl 1433.03026
[14] D. Mitchell, B. Selman, and H. Levesque. Hard and Easy Distributions of SAT Problems. In Proc. AAAI10, pages 459-465, 1992.
[15] K. D. Schild. A correspondence theory for terminological logics: preliminary report. In Proc. IJCAI12, pages 466-471, 1991. · Zbl 0742.68059
[16] R. Sebastiani. Applying GSAT to Non-Clausal Formulas. Journal of Artificial Intelligence Research, 1:309-314, 1994. · Zbl 0900.68234
[17] B. Selman, H. Levesque., and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proc. AAAI10, pages 440-446, 1992.
[18] C. B. Suttner and G. Sutcliffe. The TPTP Problem Library. Technical Report TR 95/6, James Cook University, Australia, August 1995. · Zbl 0910.68197
[19] M. Schmidt-Schauß and G. Smolka. Attributive Concept Descriptions with Complements. Artificial Intelligence, 48:1-26, 1991. · Zbl 0712.68095 · doi:10.1016/0004-3702(91)90078-X
[20] T. E. Uribe and M. E. Stickel. Ordered Binary Decision Diagrams and the Davis-Putnam Procedure. In Proc. of the 1st International Conference on Constraints in Computational Logics, 1994. · Zbl 1495.68202
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.