DIPARTIMENTO DI
INFORMATICA 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,
please contact:
pozzato[at]di.unito.it or consult the user manual.
Fig. 1: some pictures of 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.
![]() |