Focused proof systems
De Dale Miller
Apparaît dans la 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.
