Tableau-based characterization and theorem proving for default logic (Q1344885)

Ray Reiter's default logic is a propositional or predicate logic system augmented with so-called defaults. Defaults are rules of the form `if \(a\) holds and \(b\) can be consistently assumed then \(c\) can be derived', `\(b\) can be consistently assumed' means that the negation of \(b\) is not provable. This is a highly nonmonotonic system because adding new facts may prevent the application of a default rule. Moreover, one cannot do simple forward reasoning. The application of a default rule may add new facts which destroy the property that \(b\) can be consistently assumed. In the model theory of default logic there is therefore the notion of an extension. An extension is a maximally consistent set of formulae where further applications of defaults do not add new facts. A database consisting of some facts and some default rules may have no extension at all (then it is inconsistent), it may have one extension and it may have several extensions. If the basic logic is undecidable, then the extension with defaults is not even semidecidable anymore because the applicability of a default rule cannot be decided. Therefore defaults have mostly been investigated for decidable basic logics, in particular propositional logic. This paper considers default reasoning for the propositional case and briefly mentions an extension to predicate logic without function symbols, which is decidable. The authors present a method for deciding whether there are extensions of a given default theory and for computing these extensions. In contrast to previously proposed methods, which operate in a forward reasoning mode, the algorithm generates candidates for the extensions and then manipulates these candidates until extensions are obtained. The candidates are models of the basic facts, they are generated with a tableaux system, combined with models of the conclusions of the defaults. For all maximally consistent subsets of the candidates it is then checked whether the conclusions of the defaults are actually justified, i.e. whether the two preconditions hold. The algorithm is implemented in PROLOG II, but no systematic performance tests are reported.