DIPARTIMENTO   DI   INFORMATICA
Università di Torino
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, and Gian Luca Pozzato

FreeP 1.0: a Free-variables Theorem Prover for KLM Preferential Logic P of Non-monotonic reasoning

Kraus, Lehmann and Magidor (KLM) proposed a formalization of non-monotonic reasoning that was early recognized as a landmark. FreeP 1.0 is a theorem prover implementing free-variables tableaux calculi for the Preferential logic P of KLM framework. 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 FreeP 1.0. If you need some help, please contact: pozzato[at]di.unito.it or consult the user manual.

  SICStus Prolog source code
  Download the program FreeP 1.0



Fig. 1: some pictures of FreeP 1.0.


SICStus Prolog source code

  FreeP 1.0: SICStus Prolog source code

Download the program FreeP 1.0

FreeP 1.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 FreeP 1.0 shows a closed tableau of the initial set of formulas and produce a latex source file containing the same proof tree.

FreeP 1.0 (zip file, 257 kB)


How to install FreeP 1.0 (Windows, see footnote 1 below):

1. Extract FreeP 1.0.zip into a folder, for instance C:\Programs\FreeP 1.0;
2. Open file freep.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:\FreeP 1.0 with the installation directory (in the above example, C:\Programs\FreeP 1.0);
6. Run freep.bat

(1) since FreeP 1.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 Freep 1.0 you also need to install:

- 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