Skip to main content
SpringerLink
Log in

Free-Variable Tableaux for Propositional Modal Logics

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.

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. Balsinger, P., and A. Heuerding, 'Comparison of theorem provers for modal logics: Introduction and summary' in Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, LNCS 1397, Springer, 1998.

  2. Beckert, B., and R. Goré, 'Free variable tableaux for propositional modal logics' in Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Pont-à-Mousson, France, LNCS 1227, pages 91-106, Springer, 1997.

    Google Scholar 

  3. Beckert, B., and R. Goré, 'leanK 2.0:D escription for the comparison of theorem provers for modal logics' in Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, LNCS 1397, pages 33-34, Springer, 1998.

    Google Scholar 

  4. Beckert, B., and R. Goré, 'System description: lean K 2.0' in Proceedings, 15th International Conference on Automated Deduction (CADE), Lindau, Germany, LNCS 1421, pages 51-55, Springer, 1998.

    Google Scholar 

  5. Beckert, B., and R. Hähnle, 'Analytic tableaux' in W. Bibel and P. H. Schmitt, editors, Automated Deduction-A Basis for Applications, volume I:Foundations, Kluwer, Dordrecht, 1998.

    Google Scholar 

  6. Beckert, B., R. Hähnle, P. Oel, and M. Sulzmann, 'The tableau-based theorem prover 3 T A P, version 4.0' in Proceedings, 13th International Conference on Automated Deduction (CADE), New Brunswick, NJ, USA, LNCS 1104, pages 303-307, Springer, 1996.

    Google Scholar 

  7. Beckert, B., and J. Posegga, 'leanT A P:Le an tableau-based deduction' Journal of Automated Reasoning 15(3):339-358, 1995.

    Google Scholar 

  8. Bencivenga, E., 'Free logic' in D. Gabbay and F. Günthner, editors, Handbook of Philosophical Logic, volume 3, Kluwer, Dordrecht, 1986.

  9. Bonnette, N., 'K FVt : A free variable sequent system for tense logic Kt' Australian Computational Logic Workshop, February 2000.

  10. D'Agostino, M., D. Gabbay, and A. Russo, 'Grafting modalities onto substructural implication systems' Studia Logica 59:65-102, 1997.

    Google Scholar 

  11. Fitting, M., 'leanTAP revisited' Journal of Logic and Computation 8(1):33-47, 1998.

    Google Scholar 

  12. Fitting, M.C., Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library, D. Reidel, Dordrecht, Holland, 1983.

    Google Scholar 

  13. Fitting, M.C., First-Order Logic and Automated Theorem Proving, Springer, second edition, 1996.

  14. Frisch, A., and R. SCHERL, 'A general framework for modal deduction' in J. Allen, R. Fikes, and E. Sandewall, editors, Proceedings, 2nd Conference on Principles of Knowledge Representation and Reasoning, Morgan-Kaufmann, 1991.

  15. Gabbay, D., Labelled Deductive Systems, Oxford University Press, 1996.

  16. Goré, R., 'Tableau methods for modal and temporal logics' in M. D'Agostino, D. Gabbay, R. Hähnle, and J. Posegga, editors, Handbook of Tableau Methods, Kluwer, Dordrecht, 1999.

    Google Scholar 

  17. Governatori, G., 'A reduplication and loop checking free proof system for S4' in Short Papers: TABLEAUX'96, number 154-96 in RI-DSI, Via Comelico 39, 20135 Milan, Italy, 1996, Department of Computer Science, University of Milan.

    Google Scholar 

  18. Heuerding, A., M. SEYFRIED, and H. Zimmermann, 'Efficient loop-check for backward proof search in some non-classical logics' in P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proceedings, 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Terrasini, Palermo, Italy, LNCS 1071, pages 210-225, Springer, 1996.

  19. Jackson, P., and H. REICHGELT, 'A general proof method for first-order modal logic' in Proceedings, International Joint Conference on Artificial Intelligence (IJCAI), pages 942-944, 1987.

  20. Kanger, S., Provability in Logic, Stockholm Studies in Philosophy, University of Stockholm, Almqvist and Wiksell, Sweden, 1957.

    Google Scholar 

  21. Letz, R., J. SCHUMANN, S. Bayerl, and W. Bibel, 'SETHEO:A high-performance theorem prover' Journal of Automated Reasoning 8(2):183-212, 1992.

    Google Scholar 

  22. Massacci, F., 'Strongly analytic tableaux for normal modal logics' in A. Bundy, editor, Proceedings, 12th International Conference on Automated Deduction (CADE), Nancy, France, LNCS 814, pages 723-737, Springer, 1994.

  23. Massaci, F., 'Simplification:A general constraint propagation technique for propositional and modal tableaux' in Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, LNCS 1397. Springer, 1998.

  24. Mints, G., A Short Introduction to Modal Logic, CSLI, Stanford, 1992.

    Google Scholar 

  25. Otten, J., 'ileanTAP:A n intuitionistic theorem prover' in Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Pont-à-Mousson, France, LNCS 1227, Springer, 1997.

  26. Pitt, J., and J. CUNNINGHAM, 'Distributed modal theorem proving with KE' in M. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Terrasini, Palermo, Italy, LNCS 1071, pages 160-176, Springer, 1996.

  27. Reeves, S.V., 'Semantic tableaux as a framework for automated theorem-proving' in C. Mellish and J. Hallam, editors, Advances in Artificial Intelligence (Proceedings of AISB-87), pages 125-139, Wiley, 1987.

  28. Russo, A., 'Generalising propositional modal logic using labelled deductive systems' in F. Baader and K. Schulz, editors, Proceedings, Frontiers of Combining Systems (FroCoS), Munich, Germany, volume 3 of Applied Logic Series, Kluwer, Dordrecht, 1996.

    Google Scholar 

  29. Wallen, L.A., Automated Deduction in Nonclassical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics, MIT Press, 1989.

Download references

Author information

Authors and Affiliations

  1. Inst. for Logic, Complexity and Deduction Systems, University of Karlsruhe, D-76128, Karlsruhe, Germany

    Bernhard Beckert

  2. Automated Reasoning Project, Australian National University, Canberra, ACT, 0200, Australia

    Rajeev GorÉ

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rajeev GorÉ
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Beckert, B., GorÉ, R. Free-Variable Tableaux for Propositional Modal Logics. Studia Logica 69, 59–96 (2001). https://doi.org/10.1023/A:1013886427723

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1013886427723

Search

Navigation