Advertisement

System description: leanK 2.0

  • Bernhard Beckert
  • Rajeev Goré
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

Abstract

leanK is a “lean”, i.e., extremely compact, Prolog implementation of a free variable tableau calculus for propositional modal logics. leanK 2.0 includes additional search space restrictions and fairness strategies, giving a decision procedure for the logics K, KT, and S4.

Keywords

Universal Variable Expansion Rule Propositional Modal Logic Negation Normal Form Disjunctive Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    B. Beckert and R. Goré. Free variable tableaux for prepositional modal logics. In Proceedings, TABLEAUX-97, LNCS 1227, pages 91–106. Springer, 1997.Google Scholar
  2. 2.
    B. Beckert and J. Posegga. leanTAP: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.MathSciNetCrossRefGoogle Scholar
  3. 3.
    M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library. D. Reidel, Dordrecht, Holland, 1983.Google Scholar
  4. 4.
    R. Goré. Tableau methods for modal and temporal logics. In Handbook of Tableau Methods, Kluwer, Dordrecht, 1998. To appear.Google Scholar
  5. 5.
    G. Governatori. Labelled tableaux for multi-modal logics. In Proceedings, TABLEAUX-95, LNCS 918, pages 79–94. Springer, 1995.Google Scholar
  6. 6.
    J. Pitt and J. Cunningham. Distributed modal theorem proving with KE. In Proceedings, TABLEAUX-96, LNAI 1071, pages 160–176. Springer, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Bernhard Beckert
    • 1
  • Rajeev Goré
    • 2
  1. 1.Institute for Logic, Complexity and Deduction SystemsUniversity of KarlsruheKarlsruheGermany
  2. 2.Automated Reasoning Project and Department of Computer ScienceAustralian National UniversityCanberraAustralia

Personalised recommendations