Renate A. Schmidt
Skip Abstract Section
Abstract
In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable fragments of first-order logic. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that can be readily automated and is easier to deal with by existing (first-order) theorem provers than the standard translation. The principle of the axiomatic translation is conceptually very simple and can be almost completely automated. Soundness is automatic under reasonable assumptions, general decidability results can be stated and termination of ordered resolution is easily achieved. The non-trivial part of the approach is proving completeness. We prove results of completeness, decidability, model generation, the small model property and the interpolation property for a number of common and less common modal logics. We also present results of experiments with a number of first-order logic theorem provers which are very encouraging.
- Bachmair, L. and Ganzinger, H. 2001. Resolution theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, 19--99.Google Scholar
- Bachmair, L., Ganzinger, H., and Waldmann, U. 1993. Superposition with simplification as a decision procedure for the monadic class with equality. In Proceedings of the Kurt Gödel Colloquivm. Lecture Notes in Computer Science, vol. 713. Springer, 83--96. Google ScholarDigital Library
- Balbiani, P. and Herzig, A. 1994. A translation from the modal logic of provability into K4. J. Appl. Nonclassical Logics 4, 1, 73--78.Google ScholarCross Ref
- Blackburn, P., de Rijke, M., and Venema, Y. 2001. Modal Logic. Cambridge University Press. Google ScholarDigital Library
- Boy de la Tour, T. 1992. An optimality result for clause form translation. J. Symb. Computat. 14, 283--301. Google ScholarDigital Library
- Bry, F. and Yahya, A. 2000. Positive unit hyperresolution tableaux for minimal model generation. J. Autom. Reason. 25, 1, 35--82. Google ScholarDigital Library
- Castilho, M. A., Fariñas del Cerro, L., Gasquet, O., and Herzig, A. 1997. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae 3--4, 32, 281--297. Google ScholarDigital Library
- Chellas, B. F. 1980. Modal Logic: An Introduction. Cambridge University Press.Google ScholarCross Ref
- De Giacomo, G. 1996. Eliminating “converse” from converse PDL. J. Logic, Lang. Inform. 5, 2, 193--208.Google ScholarCross Ref
- De Nivelle, H. and de Rijke, M. 1999. Deciding the guarded fragments by resolution. J. Symb. Computat. To appear. Google ScholarDigital Library
- De Nivelle, H., Schmidt, R. A., and Hustadt, U. 2000. Resolution-based methods for modal logics. Logic J. IGPL 8, 3, 265--292.Google ScholarCross Ref
- Demri, S. 2001. The complexity of regularity in grammar logics and related modal logics. J. Logic Computat. 11, 6, 933--960.Google ScholarCross Ref
- Demri, S. and de Nivelle, H. 2003. Deciding regular grammar logics with converse through first-order logic. Resear. rep. LSV-03-4, Spécification et Vérification, CNRS & ENS de Cachan, France.Google Scholar
- Demri, S. and Goré, R. 1999. Tractable transformations from modal provability logics into first-order logic. In Proceedings of the International Conference on Automated Deduction (CADE-16). Lecture Notes in Artificial Intelligence, vol. 1632. Springer, 16--30. Google ScholarDigital Library
- Demri, S. and Orlowska, E. 1999. Every finitely reducible logic has the finite model property with respect to the class of ⋄-formulae. Studia Logica 62, 177--200.Google ScholarCross Ref
- Gabbay, D. M. 1975. Decidability results in nonclassical logics. Ann. Math. Logic 8, 237--295.Google ScholarCross Ref
- Ganzinger, H. and de Nivelle, H. 1999. A superposition decision procedure for the guarded fragment with equality. In Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS'99). IEEE Computer Society, 295--303. Google ScholarDigital Library
- Ganzinger, H., Meyer, C., and de Nivelle, H. 1999. The two-variable guarded fragment with transitive relations. In Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS'99). IEEE Computer Society, 24--34. Google ScholarDigital Library
- Georgieva, L., Hustadt, U., and Schmidt, R. A. 2001. Computational space efficiency and minimal model generation for guarded formulae. In Proceedings of the International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'01). Lecture Notes in Artificial Intelligence, vol. 2250. Springer, 85--99. Google ScholarDigital Library
- Georgieva, L., Hustadt, U., and Schmidt, R. A. 2002. A new clausal class decidable by hyperresolution. In Proceedings of the International Conference on Automated Deduction (CADE-18). Lecture Notes in Artificial Intelligence, vol. 2392. Springer, 260--274. Google ScholarDigital Library
- Goldblatt, R. 1987. Logics of Time and Computation. CSLI Lecture Notes, vol. 7. Chicago University Press. Google ScholarDigital Library
- Goranko, V. and Passy, S. 1992. Using the universal modality: Gains and questions. J. Logic Computat. 2, 1, 5--30.Google ScholarCross Ref
- Goré, R. 1999. Tableau methods for modal and temporal logics. In Handbook of Tableau Methods, M. D'Agostino, D. Gabbay, R. Hähnle, and J. Posegga, Eds. Kluwer, 297--396.Google Scholar
- Grädel, E. 1999. On the restraining power of guards. J. Symb. Logic 64, 1719--1742.Google ScholarCross Ref
- Hughes, G. E. and Cresswell, M. J. 1996. A New Introduction to Modal Logic. Routledge, London, UK.Google Scholar
- Hustadt, U., Dixon, C., Schmidt, R. A., and Fisher, M. 2000. Normal forms and proofs in combined modal and temporal logics. In Proceedings of FroCoS. Lecture Notes in Artificial Intelligence, vol. 1794. Springer, 73--87. Google ScholarDigital Library
- Hustadt, U. and Schmidt, R. A. 1999a. An empirical analysis of modal theorem provers. J. Appl. Nonclassical Logics 9, 4, 479--522.Google ScholarCross Ref
- Hustadt, U. and Schmidt, R. A. 1999b. Maslov's class K revisited. In Proceedings of the International Conference on Automated Deduction (CADE-16). Lecture Notes in Artifical Intelligence, vol. 1632. Springer, 172--186. Google ScholarDigital Library
- Hustadt, U. and Schmidt, R. A. 1999c. On the relation of resolution and tableaux proof systems for description logics. In Proceedings of IJCAI'99. Morgan Kaufmann, 110--115. Google ScholarDigital Library
- Hustadt, U. and Schmidt, R. A. 2000a. Issues of decidability for description logics in the framework of resolution. In Automated Deduction in Classical and Nonclassical Logics. Lecture Notes in Artificial Intelligence, vol. 1761. Springer, 191--205. Google ScholarDigital Library
- Hustadt, U. and Schmidt, R. A. 2000b. MSPASS: Modal reasoning by translation and first-order resolution. In Proceedings of TABLEAUX. Lecture Notes in Artificial Intelligence, vol. 1847. Springer, 67--71. Google ScholarDigital Library
- Hustadt, U. and Schmidt, R. A. 2002. Using resolution for testing modal satisfiability and building models. J. Autom. Reason. 28, 2, 205--232. Google ScholarDigital Library
- Kracht, M. 1995. Highway to the danger zone. J. Logic Computat. 5, 1, 93--109.Google ScholarCross Ref
- Kracht, M. 1999. Tools and Techniques in Modal Logic. Studies in Logic, vol. 142. Elsevier.Google Scholar
- Kracht, M. 2001. Reducing modal consequence relations. J. Logic Computat. 11, 6, 879--907.Google ScholarCross Ref
- Kracht, M. 2002. Notes on the space requirements for checking satisfiability in modal logics. In Advances in Modal Logic, Vol. 4, P. Balbiani, N.-Y. Suzuki, and F. Wolter, Eds. King's College Publications, London, 243--264.Google Scholar
- Kracht, M. and Wolter, F. 1997. Simulation and transfer results in modal logic---a survey. Studia Logica 59, 2, 149--177.Google ScholarCross Ref
- Leitsch, A. 1997. The Resolution Calculus. EATCS Texts in Theoretical Computer Science. Springer. Google ScholarDigital Library
- Letz, R. and Stenz, G. 2001. DCTP: A disconnection calculus theorem prover. In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'01). Lecture Notes in Artificial Intelligence, vol. 2083. Springer, 381--385. Google ScholarDigital Library
- Lewis, H. R. 1980. Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21, 317--353.Google ScholarCross Ref
- Lutz, C. 1999. Complexity of terminological reasoning revisited. In Proceeding of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'99). Lecture Notes in Artificial Intelligence, vol. 1705. Springer, 181--200. Google ScholarDigital Library
- Lutz, C. and Sattler, U. 2002. The complexity of reasoning with boolean modal logics. In Advances in Modal Logics Volume 3, F. Wolter, H. Wansing, M. de Rijke, and M. Zakharyaschev, Eds. CSLI Publications, Stanford.Google Scholar
- Massacci, F. 2000. Single step tableaux for modal logics: Computational properties, complexity and methodology. J. Autom. Reason. 24, 3, 319--364. Google ScholarDigital Library
- Nonnengart, A., Ohlbach, H. J., and Szalas, A. 1997. Quantifier elimination for second-order predicate logic. In Logic, Language and Reasoning: Essays in Honour of Dov Gabbay. To appear, Kluwer.Google Scholar
- Ohlbach, H. J. 1998. Combining Hilbert style and semantic reasoning in a resolution framework. In Proceedings of the International Conference on Automated Deduction (CADE-15). Lecture Notes in Artificial Intelligence, vol. 1421. Springer, 205--219. Google ScholarDigital Library
- Ohlbach, H. J., Nonnengart, A., de Rijke, M., and Gabbay, D. 2001. Encoding two-valued nonclassical logics in classical logic. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, 1403--1486. Google ScholarDigital Library
- Plaisted, D. A. and Greenbaum, S. 1986. A structure-preserving clause form translation. J. Symb. Computat. 2, 293--304. Google ScholarDigital Library
- Riazanov, A. and Voronkov, A. 1999. Vampire. In Proceedings of the International Conference on Automated Deduction (CADE-16). Lecture Notes in Artificial Intelligence, vol. 1632. Springer, 292--296. Google ScholarDigital Library
- Robinson, A. and Voronkov, A., Eds. 2001. Handbook of Automated Reasoning. Elsevier. Google ScholarDigital Library
- Sahlqvist, H. 1975. Completeness and correspondence in the first and second-order semantics for modal logics. In Proceedings of Scandinavian Logic Symposium 1973, S. Kanger, Ed. North-Holland, 110--143.Google ScholarCross Ref
- Schmidt, R. A. and Hustadt, U. 2000. A resolution decision procedure for fluted logic. In Proceedings of the International Conference on Automated Deduction (CADE-17). Lecture Notes in Artificial Intelligence, vol. 1831. Springer, 433--448. Google ScholarDigital Library
- Schmidt, R. A. and Hustadt, U. 2003. Mechanised reasoning and model generation for extended modal logics. In Theory and Applications of Relational Structures as Knowledge Instruments. Lecture Notes in Computer Science, vol. 2929. Springer, 38--67.Google Scholar
- Schulz, S. 2002. E: A Brainiac theorem prover. J. AI Comm. 15, 2--3, 111--126.Google Scholar
- Socher-Ambrosius, R. and Johann, P. 1997. Deduction Systems. Graduate Texts in Computer Science. Springer, New York.Google Scholar
- Stenz, G. 2002. DCTP 1.2: System abstract. In Proceedings of TABLEAUX 2002. Lecture Notes in Artificial Intelligence, vol. 2381. Springer, 335--340. Google ScholarDigital Library
- Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., and Topic, D. 2002. SPASS version 2.0. In Proceedings of the International Conference on Automated Deduction (CADE-18). Lecture Notes in Artificial Intelligence, vol. 2392. Springer, 275--279. Google ScholarDigital Library
Index Terms
- The axiomatic translation principle for modal logic
Recommendations
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsThe completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Elementary Definability and Completeness in General and Positive Modal Logic
The paper generalises Goldblatt's completeness proof for Lemmon–Scott formulas to various modal propositional logics without classical negation and without ex falso , up to positive modal logic, where conjunction and disjunction, and where necessity and ...
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
Intelligent Computer MathematicsAbstractWe formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.
Comments