Hypersequent Calculi for Propositional Default Logics

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.