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 41 articles , 1 standard article )
Showing results 1 to 20 of 41.
Sorted by year (- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
- Otten, Jens: The \textsfnanoCoP2.0 connection provers for classical, intuitionistic and modal logics (2021)
- Zese, Riccardo; Cota, Giuseppe; Lamma, Evelina; Bellodi, Elena; Riguzzi, Fabrizio: Probabilistic DL reasoning with pinpointing formulas: a Prolog-based approach (2019)
- Zese, Riccardo; Bellodi, Elena; Riguzzi, Fabrizio; Cota, Giuseppe; Lamma, Evelina: Tableau reasoning for description logics and its extension to probabilities (2018)
- Girlando, Marianna; Lellmann, Björn; Olivetti, Nicola; Pozzato, Gian Luca; Vitalis, Quentin: VINTE: an implementation of internal calculi for lewis’ logics of counterfactual reasoning (2017)
- Otten, Jens: nanoCoP: a non-clausal connection prover (2016)
- Giordano, Laura; Gliozzi, Valentina; Olivetti, Nicola; Pozzato, Gian Luca; Violanti, Luca: A multi-engine theorem prover for a description logic of typicality (2015)
- Kelly, Ryan F.; Pearce, Adrian R.: Asynchronous knowledge with hidden actions in the situation calculus (2015)
- Muskens, Reinhard; Wintein, Stefan: Analytic tableaux for all of (\mathrmSIXTEEN_3) (2015)
- Benzmüller, Christoph; Otten, Jens; Raths, Thomas: Implementing and evaluating provers for first-order modal logics (2012)
- Meissner, Adam: Experimental analysis of some computation rules in a simple parallel reasoning system for the (\mathcalALC) 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-\textsflean: 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)\textsflean\textitTAP: a declarative theorem prover for first-order classical logic (2008)
- Olivetti, Nicola; Pozzato, Gian Luca: Theorem proving for conditional logics: CondLean and \textscGoalD(\mathcalU)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)