01:34:11
publiée le 22 avril 2024
Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
From axioms to synthetic inference rules via focusing
De Dale Miller
Apparaît dans la collection : Type Theory, Constructive Mathematics and Geometric Logic / Théorie des types, mathématiques constructives et logique géométrique
Gentzen's sequent calculus can be given additional structure via focusing. We illustrate how that additional structure can be used to construct synthetic inference rules. In particular, bipolar formulas (a slight generalization of geometric formulas) can be converted to such synthetic rules once polarity is assigned to the atomic formulas and some logical connectives. Since there is some flexibility in the assignment of polarity, a given formula might yield several different synthetic rules. It is also the case that cut-elimination immediately holds for these new inference rules. Such conversion of bipolar axioms to inference rules can be done in classical and intuitionistic logics. This talk is based in part on a paper in the Annals of Pure and Applied Logic co-authored with Sonia Marin, Elaine Pimentel, and Marco Volpe (2022).
