Hypersequent calculi for propositional default logics
Andrea Sabatini
Default reasoning is a form of non-monotonic reasoning that allows to draw plausible conclusions under incomplete information and unless explicit evidence to the contrary: it can be formalized by extending classical logic with a collection of extra-logical axioms along with a set of default rules.
Starting with Reiter’s seminal work, default logic’s formalism has been investigated through Hilbert-style calculi, semantic tableaux and sequent calculi [1]. These proof-theoretic methods have undesirable features: (i) the proof-search space in Hilbert-style calculi is infinite; (ii) in tableaux-based calculi, the information flow cannot be controlled at the local level; (iii) sequent calculi rely on ad hoc extensions of the underlying language. In this talk, we introduce a novel proof-theoretic approach to default propositional logics which overcomes these drawbacks by means of a non-standard notion of hypersequent.
We redefine hypersequents as hybrid constructs, comprising sets of sequents and antisequents, and we depart from the conventional disjunctive interpretation of the separating bar, embracing a conjunctive reading: antisequents are meant to furnish contrary updates concerning the provability of the associated sequent. We employ these hybrid hypersequents to define specific extra-logical rules, which internalize within derivation trees the consistency checks involved in the application of default rules. As a result, we obtain a Gentzen-style formulation of defaults as constrained instances of Strengthening – i.e., the inverse rule of Weakening [2].
On this basis, we design hybrid hypersequent HG4 calculi for default logics: we establish admissibility of structural rules, invertibility of logical rules and a weakened version of the subformula property for cut-free proofs. We present HG4 calculi that are sound and (weakly) complete with respect to credulous consequence based over Łukasiewicz extensions [3]. Moreover, we propose a hypersequent-based decision procedure for skeptical consequence which relies on the abductive search of counterexamples [5], thereby circumventing the need for early computation of all extensions.
We conclude with a brief discussion of HG4 calculi for credulous consequence based on Reiter extensions [6], as well as for exclusionary default reasoning [4].
Bibliography
- Bonatti P. A., Olivetti N.,Sequent calculi for propositional nonmonotonic logics,ACM Transactions on Computational Logic,vol. 3 (2002), no. 2, pp. 226-278.
- Carnielli W. A., Pulcini G.,Cut-elimination and deductive polarization in complementary classical logic,Logic Journal of the IGPL,vol. 25 (2017), no. 3, pp. 273-282.
- Lukasiewicz W.,Considerations on default logic: an alternative approach,Computational Intelligence,vol. 124 (1988), no. 1, pp. 1-16.
- Horty J. F.,Reasons as defaults,Oxford University Press,2012.
- Piazza M., Pulcini G. and Sabatini A.,Abduction as deductive saturation: a proof-theoretic inquiry,Journal of Philosophical Logic,vol. 52 (2023), pp. 1575-1602.
- Reiter R.,A logic for default reasoning,Artificial Intelligence,vol. 13 (1980), no. 1-2, pp. 81-132.