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) 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.


  SICStus Prolog source code
  Java source code
  Download the program KLMLean 2.0


SICStus Prolog source code

KLMLean 2.0 implements analytic tableaux calculi for all the logics of the KLM framework:

KLMLean source code
KLM logic
SICStus Prolog source code
Rational (R)
code
Preferential (P)
code
Loop-Cumulative (CL)
code
Cumulative (C)
code



For Rational logic R, KLMLean 2.0 also implements an alternative free-variables version:

KLMLean source code
KLM logic
SICStus Prolog source code
Rational (R)
code of 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.

KLMLean 2.0 (zip file, 605 kB)


How to install KLMLean 2.0 (Windows, see footnote 1 below):

1. Extract klmlean2.0.zip into a folder, for instance C:\Programs\KLMLean 2.0;
2. Open file klmlean.bat with a text editor;
3. Replace C:\Programs\j2sdk1.4.2_13\ with your java path;
4. Replace C:\Programs\SICStus Prolog 3.12.2 with your SICStus Prolog path;
5. Replace C:\Programs\JGraphT\jgrapht-0.7.0 with your JGraphT path;
6. Replace C:\klmlean2.0 with the installation directory (in the above example, C:\Programs\KLMLean 2.0);
7. Run klm.bat

(1) since KLMLean 2.0 is implemented in Java and SICStus Prolog, one can run it on machines using any operating system. Here we only present install information for Windows since the GUI is optimized for these systems.


To run KLMLean you also need to install:

- JGraphT
- SICStus Prolog
- Java 2 Standard Edition

Remark: to compile a .tex file generated by FreeP 1.0, you need to copy the file qtree.sty in the directory containing the .tex file (http://www.ling.upenn.edu/advice/latex/qtree/).



   Back to Gian Luca Pozzato's home page