New ways for developing proof theories for first-order multi modal logics
Most of the nonclassical logics, temporal logics, process logics etc., which have been used for the specification and verification of processes are essentially extensions of modal logics. In this paper a quite complex first-order many-sorted multi modal logic (MM-Logic) with modal operators referring to a basic branching accessibility relation, its reflexive, transitive and reflexive-transitive closure, indexed modal operators, ‘eventually’ operators, ‘until’ operators and built-in equality is defined. It can serve as temporal, action, process or epistemic logic in various applications. The main purpose of this paper, however, is to demonstrate the development of a proof theory using the translation (into predicate logic) and refutation (with predicate logic resolution and paramodulation) paradigm. MM-Logic formulae are first translated into an intermediate logic called Context Logic (CL) and then with the standard translator from CL into an order-sorted predicate logic where a standard theorem prover can be used. The CL translation mechanism which simplifies the development of proof theories for complex nonclassical logics is briefly described.
KeywordsAutomated Theorem Proving by Translation and Refutation Resolution Nonclassical Logics Modal Logic Temporal Logic Process Logic Epistemic Logic Action Logic
Unable to display preview. Download preview PDF.
- Boyer&Moore 79.R.S. Boyer, J.S. Moore: A Computational Logic. Academic Press 1979.Google Scholar
- Chan 87.M. Chan. The Recursive Resolution Method. New Generation Computing, 5 pp. 155–183, 1987.Google Scholar
- Chang&Lee 73.C.-L. Chang, R.C.-T. Lee, Symbolic Logic and Mechanical Theorem Proving. Science and Applied Mathematics Series (ed. W. Rheinboldt), Academic Press, New York, 1973.Google Scholar
- Clarke&Emerson 81.M.C. Clarke, E.A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. Lecture Notes in Computer Science 131, Springer Verlag, New York, 1981, pp. 52–71.Google Scholar
- Enjalbert&Auffray 89.P. Enjalbert, Y. Auffray. Modal Theorem Proving: An Equational Viewpoint Submitted to IJCAI 89.Google Scholar
- Fariñas&Herzig 88.L. Fariñas del Cerro, A.Herzig Quantified Modal Logic and Unification Theory Langages et Systèmes Informatique, Université Paul Sabatier, Toulouse. Rapport LSI no 293, jan. 1988. See also L. Fariñas del Cerro, A. Herzig Linear Modal Deductions. Proc. of 9th Conference on Automated Deduction, pp. 487–499, 1988.Google Scholar
- Fitting 72.M.C. Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, XIII:237–247,1972.Google Scholar
- Fitting 83.M.C. Fitting. Proof methods for modal and intuitionistic logics. Vol. 169 of Synthese Library, D. Reidel Publishing Company, 1983.Google Scholar
- Grätzer 79.G. Grätzer. Universal Algebra. Springer Verlag (1979).Google Scholar
- Halpern&Moses 85.J.Y. Halpern and Y. Moses. A guide to modal logics of knowledge and belief: preliminary draft. In Proc. of 9th IJCAI, pp 479–490, 1985.Google Scholar
- Herzig 89.Herzig, A, @ PhD Thesis, Université Paul Sabatier, Toulouse.Google Scholar
- Hughes&Cresswell 68.G.E. Hughes, M.J. Cresswell. An Introduction to Modal Logics. Methuen & Co., London, 1986.Google Scholar
- Hintikka 62.J. Hintikka. Knowledge and Belief. Cornell University Press, Ithaca, New York, 1962.Google Scholar
- Konolige 86.K. Konolige. A Deduction Model of Belief and its Logics. Research Notes in Artificial Intelligence, Pitman, London, 1986.Google Scholar
- Kripke 59.S. Kripke. A Completeness Theorem in Modal Logic. J. of Symbolic Logic, Vol 24, 1959, pp 1–14.Google Scholar
- Kripke 63.S. Kripke. Semantical analysis of modal logic I, normal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, Vol. 9, 1963, pp 67–96.Google Scholar
- Levesque 84.H.J. Levesque. A logic of knowledge and active belief. Proc. of American Association of Artificial Intelligence, University of Texas, Austin 1984.Google Scholar
- Loveland 78.D. Loveland: Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science, Vol. 6, North-Holland, New York 1978.Google Scholar
- Moore 80.R.C. Moore. Reasoning about Knowledge and Action. PhD Thesis, MIT, Cambridge 1980.Google Scholar
- Ohlbach 88.H.J. Ohlbach. A Resolution Calculus for Modal Logics Thesis, FB. Informatik, University of Kaiserslautern, 1988.Google Scholar
- Ohlbach 89.H.J. Ohlbach. Context Logic. SEKI Report SR-89-8, FB. Informatik, Univ. of Kaiserslautern.Google Scholar
- Robinson 65.
- Robinson & Wos 69.Robinson, G., Wos, L. Paramodulation and theorem provcing in first order theories with equality. Machine Intelligence 4, American Elsevier, New York, pp. 135–150, 1969.Google Scholar
- Schmidt-Schauß 85.Schmidt-Schauß, M. A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. Proc. of 9th IJCAI, Los Angeles, 1985, 1162–1168.Google Scholar
- Schmidt-Schauß 88.Schmidt-Schauß, M. Computational aspects of an order-sorted logic with term declarations. Thesis, FB. Informatik, University of Kaiserslautern, 1988.Google Scholar
- Smullyan 68.R.M. Smullyan. First Order Logic, Springer Verlag, Berlin 1968.Google Scholar
- Stickel 85.
- Wallen 87.L.A. Wallen. Matrix proof methods for modal logics. In Proc. of 10th IJCAI, 1987.Google Scholar
- Walther 87.C. Walther: A Many-sorted Calculus Based on Resolution and Paramodulation. Research Notes in Artifical Intelligence, Pitman Ltd., London, M. Kaufmann Inc., Los Altos, 1987.Google Scholar