Andrea Sabatini | Searcharxiv

arXiv2026

Refutation calculi for lattice-based logics: from display to tableaux

Refutation calculi are formal systems developed to derive the invalid formulas of a given logic. While the notion of refutation calculi has played a key role in the development of tableaux calculi, a refutation approach to display calculi has not yet been attempted. In this paper, we introduce refutation display calculi for basic LE-logics, i.e., those logics canonically associated with basic normal lattice expansions of any signature. In particular, we prove soundness and completeness via proof-analysis results on derivable sequents. Finally, we obtain terminating tableaux calculi from these refutation display calculi.

math.LO↗

arXiv2025

A logic for default deontic reasoning

In many real-life settings, agents must navigate dynamic environments while reasoning under incomplete information and acting on a corpus of unstable, context-dependent, and often conflicting norms. We introduce a general, non-modal, proof-theoretic framework for deontic reasoning grounded in default logic. Its central feature is the notion of controlled sequent - a sequent annotated with sets of formulas (control sets) that prescribe what should or should not be entailed by the formulas in the antecedent. When combined with distinct extra-logical rules representing defaults and norms, these control sets record the conditions and constraints governing their applicability, thereby enabling local soundness checks for derived sequents. We prove that controlled sequent calculi satisfies admissibility of contraction and non-analytic cuts, and we establish their strong completeness with respect to credulous consequence in default theories and normative systems. Finally, we illustrate in depth how controlled sequent calculi provide a flexible and expressive basis for resolving deontic conflicts and capturing dynamic deontic notions via appropriate extra-logical rules.

cs.LO↗