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 …