Proof-Search for Normative and Doxastic Reasoning and Its Use in Logical Argumentation

Logical argumentation uses calculi to generate arguments and counter-arguments to capture defeasible reasoning. In this paper, we introduce modular proof-search procedures for a large class of such argument calculi developed to capture two core forms of defeasible reasoning: normative reasoning, formalized via input/output logics, and doxastic reasoning, formalized via normal default logic. Our approach relies on modular, rule-based, and terminating decomposition trees via step-by-step decomposition of norms and defaults. When successful, a terminated decomposition tree certifies derivability of a given argument in its corresponding calculus, including arguments for obligations and beliefs, as well as defeating arguments concluding inapplicability of norms and defaults. We show how rule-based decomposition of norms and defaults is used to determine nonmonotonic inference for credulous reasoning with maximal consistent sets of norms and defaults as well as stable sets of arguments in formal argumentation.