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

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

Organisateur(s) Tortora de Falco, Lorenzo ; Vaux Auclair, Lionel
Date(s) 24/01/2022 - 28/01/2022
URL associée https://conferences.cirm-math.fr/2685.html
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.

Informations sur la vidéo

Données de citation

Bibliographie

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

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow




Inscrivez-vous

  • Mettez des vidéos en favori
  • Ajoutez des vidéos à regarder plus tard &
    conservez votre historique de consultation
  • Commentez avec la communauté
    scientifique
  • Recevez des notifications de mise à jour
    de vos sujets favoris
Donner son avis