A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules

Since introduced by Reiter in his seminal 1980 paper: ‘A Logic for Default Reasoning’, the subject of reasoning with default rules has been extensively dealt with in the literature on nonmonotonic reasoning. Yet, with some notable exceptions, the same cannot be said about its proof theory. Aiming to contribute to the latter, we propose a tableaux based proof calculus for a propositional variant of Reiter’s presentation of reasoning with default rules. Our tableaux based proof calculus is based on a reformulation of the semantics of Reiter’s view of a default theory, i.e., a tuple comprised of a set of sentences and a set of default rules, as a premiss structure. In this premiss structure, sentences stand for definite assumptions, as normally found in the literature, and default rules stand for tentative assumptions, as opposed to rules of inference, as normally found in the literature. On this basis, a default consequence is defined as being such relative to a premiss structure, as is our notion of a default tableaux proof. In addition to its simplicity, as usual in tableaux based proof calculi, our proof calculus allows for the discovery of the non-existence of proofs by providing corresponding counterexamples.