Return
A unified framework for Input/Output and default logics via hypersequents
M
S
DOI:10.1093/logcom/exag006.png)
Abstract
En 中文
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.
Keywords:
Input/output logic
default logics
hypersequent calculi
proof-theory for non-classical logics
Journal
J
IF:
0
Papers:
44
Citations:
0
