Linear Logic Winter School / École d'hiver de logique linéaire

Collection Linear Logic Winter School / École d'hiver de logique linéaire

Organizer(s) Tortora de Falco, Lorenzo ; Vaux Auclair, Lionel
Date(s) 1/24/22 - 1/28/22
linked URL
00:00:00 / 00:00:00
4 6

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.

Information about the video

Citation data


  • LIANG, Chuck et MILLER, Dale. Focusing Gentzen's LK proof system. 2021. To appear for in the volume Peter Schroeder-Heister on 'Proof- Theoretic Semantics' within the Springer Outstanding Contributions to Logic series. -

Last related questions on MathOverflow

You have to connect your account with mathoverflow to add question

Ask a question on MathOverflow


  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
  • Get notification updates
    for your favorite subjects
Give feedback