ModLeanTAP: Lean Tableau-based Deduction for Propositional Modal Logics. ModLeanTAP is a lean Prolog implementation of a modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal variables), which has been developed by Bernhard Beckert and Rajeev Goré. ModLeanTAP is not only surprisingly short, but compares favourably with other considerably more complex implementations for modal deduction. ModLeanTAP’s development was inspired by the lean tableau-based prover for first-order logic leanTAP. ModLeanTAP Version 2.0 includes additional search space restrictions and fairness strategies, giving a decision procedure for the logics K, KD, KT, and S4

References in zbMATH (referenced in 17 articles )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Otten, Jens: MleanCoP: a connection prover for first-order modal logic (2014)
  2. Pozzato, Gian Luca: Conditional and preferential logics. Proof methods and theorem proving. (2010)
  3. Antonsen, Roger; Waaler, Arild: Liberalized variable splitting (2007)
  4. Giordano, Laura; Gliozzi, Valentina; Pozzato, Gian Luca: KLMLean 2.0: A theorem prover for KLM logics of nonmonotonic reasoning (2007)
  5. Formisano, Andrea; Nicolosi-Asmundo, Marianna: An efficient relational deductive system for propositional non-classical logics (2006)
  6. Goranko, V.; Montanari, A.; Sala, P.; Sciavicco, G.: A general tableau method for propositional interval temporal logics: theory and implementation (2006)
  7. Olivetti, Nicola; Pozzato, Gian Luca: CondLean 3.0: Improving CondLean for stronger conditional logics (2005)
  8. Nabeshima, Hidetomo; Iwanuma, Koji; Inoue, Katsumi: SOLAR: a consequence finding system for advanced reasoning (2003)
  9. Patel-Schneider, P. F.; Sebastiani, R.: A new general method to generate random modal formulae for testing decision procedures (2003)
  10. Artosi, Alberto; Governatori, Guido; Rotolo, Antonino: Labelled tableaux for nonmonotonic reasoning: Cumulative consequence relations (2002)
  11. Thion, V.; Cerrito, S.; Cialdea Mayer, Marta: A general theorem prover for quantified modal logics (2002)
  12. Beckert, Bernhard; Goré, Rajeev: Free-variable tableaux for propositional modal logics (2001)
  13. Horrocks, Ian; Patel-Schneider, Peter F.; Sebastiani, Roberto: An analysis of empirical testing for modal decision procedures (2000)
  14. Demri, Stéphane: Sequent calculi for nominal tense logics: A step towards mechanization? (1999)
  15. Kreitz, Christoph; Otten, Jens: Connection-based theorem proving in classical and non-classical logics (1999)
  16. Mantel, Heiko; Otten, Jens: linTAP: A tableau prover for linear logic (1999)
  17. Massacci, Fabio: Tableau methods for formal verification of multi-agent distributed systems (1998)