01:34:11
published on April 22, 2024
Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
By Marie Kerjean
Focused proof systems
By Dale Miller
Appears in collection : Linear Logic Winter School / École d'hiver de logique linéaire
Gentzen's sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut-elimination and consistency for classical and intuitionistic logics. Among the undesirable features of sequent calculi is the fact that their inferences rules are very low-level. We present the focused proof system LKF in which synthetic inference rules can systematically be defined and for which cut-eliminate hold.
