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.

Abstract Constrained Input/Output (I/O) logics address scenarios involving conflicting conditional obligations. By allowing the withdrawal of norms to preserve consistency, these logics exhibit a close relationship with default logics. In this paper, we provide a formal account of this relationship to develop a uniform Gentzen-style proof theory for the entire family of constrained I/O logics under the credulous approach. Specifically, we introduce hypersequent calculi that integrate extra-logical rules to directly capture conditional obligations. The parallel composition of sequents and antisequents formalizes the dynamic updating of conclusions under consistency constraints. Crucially, such an approach avoids any ad hoc extension of the underlying language. Moreover, we establish the admissibility of structural rules and the invertibility of logical rules, showing that cut-free proofs maintain a weakened form of analyticity. Finally, we leverage straightforward translations between hypersequent calculi for constrained I/O logics and those for default logics, as developed in Piazza and Sabatini (2025, ACM Trans. Comput. Log., 26, 1–36), to provide a modular treatment of disjunctive default logics and disjunctive normative inference.

In this article, we investigate default reasoning from a structural proof-theoretic perspective. We introduce hybrid hypersequent calculi for propositional default logics, where extra-logical rules directly capture default rules, while parallel composition of sequents and antisequents formalizes contrary updating on the conclusions of extra-logical rules. We establish the admissibility of structural rules and the invertibility of logical rules, showing that cut-free proofs exhibit a weakened form of analyticity. Next, we prove that specific hybrid hypersequent calculi are sound and weakly complete with respect to credulous consequence based on Łukaszewicz extensions. Lastly, we propose a hypersequent-based decision method for skeptical consequence which circumvents the need for early computation of all extensions.