A tableaux-based theorem prover for a decidable subset of default logic

Abstract

We present a new, efficient and clear method for computing extensions and deriving formulas of a normal default theory which offers a new insight into the nature of default reasoning and seems to be equally successfully applicable to open and non-normal default theories. It is based on the semantic tableaux method (Smullyan 1968) and works for default theories with a finite set of defaults which are formulated over a decidable subset of first-order logic. We prove that all extensions of a normal default theory can be produced by constructing the semantic tableau of one formula built from the general laws and the default consequences.