TABLEAUX: A general theorem prover for modal logics. (English) Zbl 0743.03008
Summary: We present a general theorem proving system for propositional modal logics, called TABLEAUX. The main feature of the system is its generality, since it provides a unified environment for various kinds of modal operators and for a wide class of modal logics, including usual temporal, epistemic or dynamic logics. We survey the modal languages covered by TABLEAUX, which range from the basic one \(L(\square,\lozenge)\) through a complex multimodal language including several families of operators with their transitive closure and converse. The decision procedure we use is basically a semantic tableaux method, but with slight modifications compared to the traditional one. We emphasize the advantages of such semantical proof methods for modal logics, since we believe that the model construction they provide represents perhaps the most attractive feature of these logics for possible applications in computer science and AI. The system has been implemented in Prolog, and appears to be of reasonable efficiency for most current examples. Experimental results are given, with two lists of test examples.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03-04 | Software, source code, etc. for problems pertaining to mathematical logic and foundations |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B45 | Modal logic (including the logic of norms) |
Keywords:
experimental results; temporal logic; dynamic logic; epistemic logic; general theorem proving system; propositional modal logics; multimodal language; decision procedure; semantic tableaux; Prolog; test examplesReferences:
| [1] | Abadi, M. and Manna, Z., ’Modal theorem proving’,Lecture Notes in Computer Science Vol. 230 (1986). · Zbl 0626.68065 |
| [2] | Abadi, M. and Manna, Z., ’Temporal logic programming’,Proc. IEEE Symposium on Logic Programming (Sept. 1987) San Francisco, California, pp. 4–16. |
| [3] | VanBenthem J.,The Logic of Time, D. Reidel, Dordrecht (1980). |
| [4] | Ben-Ari, M., Manna, Z. and Pnueli, A., ’The temporal logic of branching time’,Proc. 8th Annual ACM Symposium on Principles of Programming Languages (1981), pp. 164–176. · Zbl 0533.68036 |
| [5] | Bull, R. and Segerberg, K., ’Basic modal logic’ in [28], pp. 1–88. · Zbl 0875.03045 |
| [6] | Burgess, J. P., ’Decidability for branching time’,Studia Logica 39 (2/3), (1980). · Zbl 0467.03006 |
| [7] | Catach, L., ’Normal multimodal logics’,Proc. AAAI’88, pp. 491–495. |
| [8] | Catach, L., ’Les logiques multimodales’ (’Multimodal logics’), Doctoral Thesis, IBM Paris Scientific Center and L.I.T.P., Paris 6 University (1989). |
| [9] | Clarke E. M. and Emerson E. A., ’Design and synthesis of synchronization skeletons using branching time temporal logic’,Lecture Notes in Computer Science Vol. 131 (1982), pp. 52–71. · Zbl 0546.68014 · doi:10.1007/BFb0025774 |
| [10] | Clarke, E. M., Emerson, E. A., and Sistla, A. P., ’Automatic verification of finite-state concurrent systems using temporal logic specifications’,ACM Transactions on Programming Languages and Systems,8(2) (1986). · Zbl 0591.68027 |
| [11] | Chellas, B. F.,Modal Logic. An Introduction, Cambridge University Press (1980). · Zbl 0431.03009 |
| [12] | Cavalli A. and Horn F., ’Evaluation des spécifications formelles à l’aide des automates finis et de la logique temporelle’, Report L.I.T.P. No. 86-74, Paris VI/Paris VII University, France (1986). |
| [13] | Enjalbert, P. and Auffray, Y., ’Démonstration de théorèmes en logique modale: un point de vue équationnel’,European Workshop on Logical Methods in Artificial Intelligence (JELIA’88), Roscoff, France (1988). |
| [14] | Enjalbert P. and Fariñas L., ’Modal Resolution in clausal form’, Report No. RG 14-86, Greco de Programmation, Université de Bordeaux I, France (1986). · Zbl 0669.03009 |
| [15] | Emerson E. A. and Halpern J. Y. ’Decision procedures and expressiveness in the temporal logic of branching time’,Journal of Computer and System Sciences 30, 1–24 (1985). · Zbl 0559.68051 · doi:10.1016/0022-0000(85)90001-7 |
| [16] | Emerson E. A., ’Automata, tableaux and temporal logics’,Lecture Notes in Computer Science Vol. 193 (1985), pp. 79–87. · Zbl 0603.03005 |
| [17] | Emerson E. A. and Sistla A. P., ’Deciding full branching time logic’,Information and Control 61, 175–201 (1984). · Zbl 0593.03007 · doi:10.1016/S0019-9958(84)80047-9 |
| [18] | Fariñas Del Cerro, L., ’Resolution modal logic’,Logique et Analyse 110–111 (1985). · Zbl 0631.03007 |
| [19] | Fischer M. J. and Immerman N., ’Interpreting logics of knowledge in propositional dynamic logic with converse’,Information Processing Letters 25 175–181 (1987). · Zbl 0634.03012 · doi:10.1016/0020-0190(87)90129-3 |
| [20] | Fitting M., ’Tableaux methods of proof for modal logics’,Notre-Dame Journal of Formal Logic 13 237–247 (1972). · doi:10.1305/ndjfl/1093894722 |
| [21] | Fitting, M., ’Proof methods for modal and intuitionistic logics’, Reidel,Synthese Library Vol. 169 (1983). · Zbl 0523.03013 |
| [22] | Fischer M. J. and Ladner R. E., ’Propositional dynamic logic of regular programs,Journal of Computer and System Sciences 18 194–211 (1979). · Zbl 0408.03014 · doi:10.1016/0022-0000(79)90046-1 |
| [23] | Fujita, M.et al. ’Tokyo: logic programming language based on temporal logic’,Proc. 3th International Conference on Logic Programming, London pp. 695–709 (1986). |
| [24] | Gabbay, D. M., ’Modal and temporal logic programming’, inTemporal Logics, A. Galton (ed.), Academic Press (1988). |
| [25] | Groeneboer, C. and Delgande, J. P., ’Tableau-based theorem proving in normal conditional logics’,Proc. AAAI’88, pp. 171–176. |
| [26] | Gurevich, Y. and Shelah, S., ’The decision problem for Branching Time Logic’,Journal of Symbolic Logic 50(3) (1985). · Zbl 0584.03006 |
| [27] | Halpern, J. Y., ’Reasoning about knowledge: an overview’,Proc. Conference on Theoretical Aspects of Reasoning about Knowledge (J. Y. Halpern (ed.)), Morgan Kauffmann (1986). |
| [28] | ’Extensions of classical logic’,Handbook of Philosophical Logic Vol. II, D. Gabbay and F. Guenthner (eds.), D. Reidel Publishing Company (1984). · Zbl 0572.03003 |
| [29] | Harel, D., ’Dynamic logic’, in [28], pp. 497–604. · Zbl 0875.03076 |
| [30] | Hughes G. E. and Cresswell M. J.,An Introduction to Modal Logic, Methuen, London (1968). · Zbl 0205.00503 |
| [31] | Halpern, J. Y. and Moses, Y., ’A guide to the modal logics of knowledge and belief’,Proc. IJCAI pp. 480–490 (1985). |
| [32] | Halpern J. Y. and Shoham Y., ’A propositional modal logic of time intervals’,Proc. IEEE Symposium on Logic in Computer Science Vol. 1 pp. 279–292 (1986). |
| [33] | Jackson, P. and Reichgelt, H., ’A general proof method for first-order modal logic’,Proc. IJCAI pp. 942–944 (1987). |
| [34] | Jackson, P. and Reichgelt, H. ’A general proof method for modal predicate logic without the Barcan formula’,Proc. AAAT’88, pp. 177–181 (1988). |
| [35] | Konolige K., ’Resolution and quantified epistemic logics’,Lectures Notes in Computer Science Vol. 230 pp. 199–208 (1986). · Zbl 0626.68066 |
| [36] | Ladner R. E., ’The computational complexity of provability in systems of modal propositional logic’,SIAM J. Computing 6(3) 467–480 (1977). · Zbl 0373.02025 · doi:10.1137/0206033 |
| [37] | Lehmann D. and Kraus S., ’Knowledge, belief and time’,Lecture Notes in Computer Science, Vol. 226 pp. 186–195 (1986). |
| [38] | Lafon, E. and Schwind, C. B., ’A theorem prover for action performance’,Proc. ECAI’88 (1988). |
| [39] | Michel, M., ’Computation of temporal operators’,Logique et Analyse 110/111 (1985). |
| [40] | Moszkowski, B.,Executing temporal logic of programs, Cambridge University Press (1986). · Zbl 0565.68003 |
| [41] | Manna, Z. and Wolper, P., ’Synthesis of communicating processes from temporal logic specifications’, Report No. STAN-CS-81-872, Stanford University, Dept. of Computer Science (1981). · Zbl 0522.68030 |
| [42] | Niemela, I. and Tuominen, H., ’Helsinki logic machine: a system for logical expertise’, Technical report Series B (No. 1), Helsinki University of Technology, Digital Systems Laboratory (1987). |
| [43] | Parikh R., ’Propositional dynamic logics of programs: a survey’,Lecture Notes in Computer Science Vol. 125 pp. 102–144 (1981). · Zbl 0468.68038 |
| [44] | Plaisted D. A., ’A decision procedure for combinations of propositional temporal logic and other specialized theories’,J. Automated Reasoning 2, 171–190 (1986). · Zbl 0635.03026 · doi:10.1007/BF02432150 |
| [45] | Pnueli, A., ’The temporal logic of programs’,Proc. 18th IEEE Symposium on Foundations of Computer Science pp. 46–57 (1977). |
| [46] | Pratt, V. R., ’Models of program logics’,Proc. 20th IEEE Symposium on Foundations of Computer Science (1978). · Zbl 0364.68012 |
| [47] | IBM, VM/Programming in Logic (VM/Prolog), Program Offering 5785-ABH. |
| [48] | Roche Y., ’Implémentation d’un démonstrateur de théorèmes pour les logiques modales et temporelles en Prolog’, Report GIA-GRTC, Luminy University, Marseille, France (1985). |
| [49] | Rescher, N. and Urquhart, A.,Temporal Logic, Springer-Verlag (1971). · Zbl 0229.02027 |
| [50] | Sistla, A. P. and Clarke, E. M., ’The complexity of Propositional linear temporal logics’,J. ACM 32(3) (1985). · Zbl 0632.68034 |
| [51] | Schwind, C., ’Un démonstrateur de théorèmes pour des logiques modales et temporelles en Prolog’,Proc. 5th. Congrès Reconnaissance des Formes et Intelligence Artificielle (RFIA), France pp. 897–914 (1985). |
| [52] | Smullyan, R. M.,First-Order Logic, Springer-Verlag (1968). · Zbl 0172.28901 |
| [53] | Thistlewaite P. B., McRobbie M. A., and Meyer R. K., ’The KRIPKE automated theorem proving system’,Lecture Notes in Computer Science Vol. 230 pp. 705–706 (1986). |
| [54] | Venema, Y., ’Expressiveness and completeness of an interval tense logic’, Report, Institute for Language, Logic and Information, University of Amsterdam (1988). · Zbl 0725.03006 |
| [55] | Yardi, M. Y. and Wolper, P., ’Automata theoretic techniques for modal logics of programs’,Proc. ACM Symposium on Theory of Computing (1984). |
| [56] | Wallen, L. A., Matrix proof methods for modal logics’,Proc. IJCAI pp. 917–923 (1987). |
| [57] | Wolper, P., ’Temporal logic can be more expressive’,Information and Control 56 (1983). · Zbl 0534.03009 |
| [58] | Wolper, P., ’The tableaux method for temporal logic: an overview’,Logique et Analyse 110–111 (1985). · Zbl 0585.03008 |
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.
