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; 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.68097Beckert, Bernhard; Posegga, Joachim 1995 all top 5 Cited by 57 Authors 6 Otten, Jens 6 Pozzato, Gian Luca 5 Beckert, Bernhard 5 Goré, Rajeev Prabhakar 5 Olivetti, Nicola 3 Posegga, Joachim 2 Bellodi, Elena 2 Cota, Giuseppe 2 Giordano, Laura 2 Gliozzi, Valentina 2 Lamma, Evelina 2 Riguzzi, Fabrizio 2 Zese, Riccardo 1 Abate, Pietro 1 Alenda, Régis 1 Avron, Arnon 1 Benzmüller, Christoph Ewald 1 Bibel, Wolfgang 1 Bonnette, Nicolette 1 Byrd, William E. 1 de Rijke, Maarten 1 Färber, Michael 1 Ferré, Sébastien 1 Fitting, Melvin Chris 1 Friedman, Daniel P. 1 Girlando, Marianna 1 Golińska-Pilarek, Joanna 1 Honsell, Furio 1 Inoue, Katsumi 1 Iwanuma, Koji 1 Kaliszyk, Cezary 1 Kelly, Ryan F. 1 Konrad, Karsten 1 Lellmann, Björn 1 Letz, Reinhold 1 Mantel, Heiko 1 Meissner, Adam 1 Miculan, Marino 1 Monz, Christof 1 Mora, Angel 1 Muñoz-Velasco, Emilio 1 Muskens, Reinhard A. 1 Nabeshima, Hidetomo 1 Near, Joseph P. 1 Paravano, Cristian 1 Pearce, Adrian R. 1 Peltier, Nicolas 1 Raths, Thomas 1 Ridoux, Olivier 1 Schmitt, Stephan 1 Stenz, Gernot 1 Urban, Josef 1 Veroff, Robert 1 Violanti, Luca 1 Vitalis, Quentin 1 Weidenbach, Christoph 1 Wintein, Stefan all top 5 Cited in 12 Serials 3 Journal of Automated Reasoning 2 Studia Logica 1 Artificial Intelligence 1 Journal of Philosophical Logic 1 The Journal of Logic Programming 1 Journal of Symbolic Computation 1 Journal of Logic and Computation 1 International Journal of Computer Mathematics 1 Journal of Applied Non-Classical Logics 1 Annals of Mathematics and Artificial Intelligence 1 International Journal of Applied Mathematics and Computer Science 1 Theory and Practice of Logic Programming Cited in 4 Fields 35 Computer science (68-XX) 23 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year