Università di Torino
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,
pozzato[at]di.unito.it or consult the user manual.
Fig. 1: some pictures of 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.
Back to Gian Luca Pozzato's home page