leanTAP
leanTAP revisited. The Prolog program leanTAP is a theorem prover for first order logic that is complete. This program, which has been created by Beckert and Posegga, is remarkably short. In this paper, the author shows that leanTAP can be understood by viewing it as the implementation of a sequent calculus. He shows correctness and completeness of this calculus. Since the correspondence between the sequent calculus and the program leanTAP is evident, this in turn constitutes a proof of the correctness of leanTAP. Next, the author generalizes the sequent calculus to the modal logic K and sketches a proof of the completeness of this sequent calculus. Then, the author transforms the sequent calculus back into a Prolog program. Doing this, he arrives at a theorem prover for the modal logic K which is as elegant as leanTAP. Following that, he sketches how similar results can be obtained for the modal logics T, K4 and S4. The paper is restricted to the propositional case. The author claims that the results can be extended to the case of quantified modal logics as long as the Barcan formula is not assumed. The paper is very well written and a pleasure to read.
Keywords for this software
References in zbMATH (referenced in 29 articles , 1 standard article )
Showing results 1 to 20 of 29.
Sorted by year (- Kelly, Ryan F.; Pearce, Adrian R.: Asynchronous knowledge with hidden actions in the situation calculus (2015)
- Meissner, Adam: Experimental analysis of some computation rules in a simple parallel reasoning system for the $\calALC$ description logic (2011)
- Mora, A.; Muñoz-Velasco, E.; Golińska-Pilarek, J.: Implementing a relational theorem prover for modal logic K (2011)
- Alenda, Régis; Olivetti, Nicola; Pozzato, Gian Luca: CSL-\ssflean: a theorem-prover for the logic of comparative concept similarity (2010)
- Abate, Pietro; Goré, Rajeev: The Tableau Workbench (2009)
- Byrnes, John; Buchanan, Michael; Ernst, Michael; Miller, Philip; Roberts, Chris; Keller, Robert: Visualizing proof search for theorem prover development (2009) ioport
- Near, Joseph P.; Byrd, William E.; Friedman, Daniel P.: $\alpha$\ssflean\itTAP: a declarative theorem prover for first-order classical logic (2008)
- Olivetti, Nicola; Pozzato, Gian Luca: Theorem proving for conditional logics: CondLean and GoalD$\cal U$CK (2008)
- Cederquist, J.G.; Corin, R.; Dekker, M.A.C.; Etalle, S.; Den Hartog, J.I.; Lenzini, G.: Audit-based compliance control (2007) ioport
- Giordano, Laura; Gliozzi, Valentina; Pozzato, Gian Luca: KLMLean 2.0: A theorem prover for KLM logics of nonmonotonic reasoning (2007)
- Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
- Olivetti, Nicola; Pozzato, Gian Luca: CondLean 3.0: Improving CondLean for stronger conditional logics (2005)
- Peltier, Nicolas: Some techniques for branch-saturation in free-variable tableaux (2004)
- Nabeshima, Hidetomo; Iwanuma, Koji; Inoue, Katsumi: SOLAR: a consequence finding system for advanced reasoning (2003)
- Otten, Jens; Bibel, Wolfgang: IeanCOP: lean connection-based theorem proving (2003)
- Ferré, Sébastien; Ridoux, Olivier: A framework for developing embeddable customized logics (2002)
- Beckert, Bernhard; Goré, Rajeev: Free-variable tableaux for propositional modal logics (2001)
- Schmitt, Stephan: A tableau-like representation framework for efficient proof reconstruction (2000)
- Goré, Rajeev: Tableau methods for modal and temporal logics (1999)
- Mantel, Heiko; Otten, Jens: linTAP: A tableau prover for linear logic (1999)