DIPARTIMENTO DI
INFORMATICA
Università di Torino | |

Laura Giordano, Valentina Gliozzi, and Gian Luca Pozzato
KLMLean 2.0: a Theorem Prover for KLM Logics of Non-monotonic reasoning
Kraus, Lehmann and Magidor (KLM) proposed a formalization of non-monotonic reasoning that was early recognized
as a landmark. KLMLean 2.0 is a theorem prover implementing analytic tableaux calculi for all the logics
of the KLM framework, namely (from the stringest to the weakest) Fig. 1: some pictures of KLMLean 2.0.
SICStus Prolog source code Java source code Download the program KLMLean 2.0
KLMLean 2.0 implements analytic tableaux calculi for all the logics of the KLM framework:
For Rational logic R, KLMLean 2.0 also implements an alternative free-variables version:
Download the program KLMLean 2.0
KLMLean 2.0 comprises a graphical interface written in Java. One can prove if a formula
can be derived by a knowledge base by putting them into the text fields and then clicking a button. If
one can infer the formula from the inserted knowledge base, then KLMLean 2.0 shows a closed tableau of the
initial set of formulas and produce a latex source file containing the same proof tree.
Back to Gian Luca Pozzato's home page |