An Implementation of a Free-variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: the Theorem Prover FreeP 1.0
Laura Giordano, Valentina Gliozzi, Nicola Olivetti and Gian Luca Pozzato
The 10th Congress of the Italian Association for Artificial Intelligence (AIIA 2007)
Roma, Italy, September 10-13, 2007
Abstract
In this work we present FreeP 1.0, a theorem prover for the KLM preferential logic P of nonmonotonic reasoning. FreeP 1.0 is a SICStus Prolog implementation of a free-variables, labelled tableau calculus for P, obtained by introducing suitable modalities to interpret conditional assertions. The performances of FreeP 1.0 are promising. FreeP 1.0 can be downloaded at http://www.di.unito.it/FreeP 1.0