Skip to main content
SpringerLink
Log in

TABLEAUX: A general theorem prover for modal logics

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

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 an 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(□, ◊) 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 models 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 in the paper, with two lists of test examples.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi, M. and Manna, Z., ‘Modal theorem proving’,Lecture Notes in Computer Science Vol. 230 (1986).

  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).

    Google Scholar 

  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.

  5. Bull, R. and Segerberg, K., ‘Basic modal logic’ in [28], pp. 1–88.

  6. Burgess, J. P., ‘Decidability for branching time’,Studia Logica 39 (2/3), (1980).

  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.

    Google Scholar 

  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).

  11. Chellas, B. F.,Modal Logic. An Introduction, Cambridge University Press (1980).

  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).

    Google Scholar 

  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).

    Google Scholar 

  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).

    Article  Google Scholar 

  16. Emerson E. A., ‘Automata, tableaux and temporal logics’,Lecture Notes in Computer Science Vol. 193 (1985), pp. 79–87.

    Google Scholar 

  17. Emerson E. A. and Sistla A. P., ‘Deciding full branching time logic’,Information and Control 61, 175–201 (1984).

    Article  Google Scholar 

  18. Fariñas Del Cerro, L., ‘Resolution modal logic’,Logique et Analyse 110–111 (1985).

  19. Fischer M. J. and Immerman N., ‘Interpreting logics of knowledge in propositional dynamic logic with converse’,Information Processing Letters 25 175–181 (1987).

    Article  Google Scholar 

  20. Fitting M., ‘Tableaux methods of proof for modal logics’,Notre-Dame Journal of Formal Logic 13 237–247 (1972).

    Google Scholar 

  21. Fitting, M., ‘Proof methods for modal and intuitionistic logics’, Reidel,Synthese Library Vol. 169 (1983).

  22. Fischer M. J. and Ladner R. E., ‘Propositional dynamic logic of regular programs,Journal of Computer and System Sciences 18 194–211 (1979).

    Article  Google Scholar 

  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).

  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).

  29. Harel, D., ‘Dynamic logic’, in [28], pp. 497–604.

  30. Hughes G. E. and Cresswell M. J.,An Introduction to Modal Logic, Methuen, London (1968).

    Google Scholar 

  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).

    Google Scholar 

  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).

    Google Scholar 

  36. Ladner R. E., ‘The computational complexity of provability in systems of modal propositional logic’,SIAM J. Computing 6(3) 467–480 (1977).

    Article  Google Scholar 

  37. Lehmann D. and Kraus S., ‘Knowledge, belief and time’,Lecture Notes in Computer Science, Vol. 226 pp. 186–195 (1986).

    Google Scholar 

  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).

  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).

  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).

    Google Scholar 

  44. Plaisted D. A., ‘A decision procedure for combinations of propositional temporal logic and other specialized theories’,J. Automated Reasoning 2, 171–190 (1986).

    Google Scholar 

  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).

  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).

    Google Scholar 

  49. Rescher, N. and Urquhart, A.,Temporal Logic, Springer-Verlag (1971).

  50. Sistla, A. P. and Clarke, E. M., ‘The complexity of Propositional linear temporal logics’,J. ACM 32(3) (1985).

  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).

  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).

    Google Scholar 

  54. Venema, Y., ‘Expressiveness and completeness of an interval tense logic’, Report, Institute for Language, Logic and Information, University of Amsterdam (1988).

  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).

  58. Wolper, P., ‘The tableaux method for temporal logic: an overview’,Logique et Analyse 110–111 (1985).

Download references

Author information

Authors and Affiliations

  1. IBM Paris Scientific Center, LITP-Paris 6 University, France

    Laurent Catach

Authors
  1. Laurent Catach
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

A preliminary version of this paper appeared in the Proceedings of the International Computer Science Conference (ICSC'88), Hong-Kong, December 19–21, 1988.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Catach, L. TABLEAUX: A general theorem prover for modal logics. J Autom Reasoning 7, 489–510 (1991). https://doi.org/10.1007/BF01880326

Download citation

  • Received:

  • Accepted:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01880326

Key words

Search

Navigation