leanTAP
swMATH ID:  9985 
Software Authors:  Beckert, Bernhard; Posegga, Joachim 
Description:  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. 
Homepage:  http://formal.iti.kit.edu/beckert/leantap/ 
Keywords:  modal logic; automatic theorem proving; leanTAP; sequent calculus; correctness; completeness 
Related Software:  SETHEO; TPTP; SATCHMO; ModLeanTAP; ileanCoP; leanCoP; CondLean; 3TAP; nanoCoP; MleanCoP; FEMaLeCoP; OTTER; Twelf; KLMLean; HARP; ESETHEO; QMLTP; ILTP; OntoDLV; KLONE 
Cited in:  39 Publications 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

lean\(T^ AP\): Lean tableaubased deduction. Zbl 0838.68097 Beckert, Bernhard; Posegga, Joachim 
1995

all
top 5
Cited by 57 Authors
all
top 5
Cited in 12 Serials
Cited in 4 Fields
35  Computer science (68XX) 
23  Mathematical logic and foundations (03XX) 
1  General and overarching topics; collections (00XX) 
1  Information and communication theory, circuits (94XX) 