Tableau-based characterization and theorem proving for default logic

In this paper, we present a new method for computing extensions and for deriving formulae from a default theory. It is based on the semantic tableaux method and works for default theories with a finite set of defaults that are formulated over a decidable subset of first-order logic. We prove that all extensions (if any) of a default theory can be produced by constructing the semantic tableau ofone formula built from the general laws and the default consequences. This result allows us to describe an algorithm that provides extensions if there are any, and to decide if there are none. Moreover, the method gives a necessary and sufficient criterion for the existence of extensions of default theories with finitely many defaults provided they are formulated on a decidable subset of FOL.This work was completed while the author was at CNRS, Marseille.