An Implementation of a Free-Variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: The Theorem Prover FreeP 1.0

摘要

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.