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; E-SETHEO; QMLTP; ILTP; OntoDLV; KL-ONE
Cited in: 39 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
lean\(T^ AP\): Lean tableau-based deduction. Zbl 0838.68097
Beckert, Bernhard; Posegga, Joachim

Citations by Year