Università di Torino
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) rational logic R,
preferential logic P, loop-cumulative logic CL, and cumulative logic C. It is
written in SICStus Prolog and also comprises a GUI written in Java.
In this page you will find all you need to run and use KLMLean 2.0. If you need some help,
pozzato[at]di.unito.it or consult the user manual.
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:
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