The cut-elimination theorem, also known as Gentzen's Hauptsatz, is a fundamental result in the sequent calculus. It was first proven by Gerhard Gentzen in 1934 for intuitionistic and classical logic systems. The theorem states that any judgement with a proof using the cut rule can also be proven without using the cut rule.
Carnegie Mellon University
Fall 2021
This undergraduate course introduces students to constructive logics such as intuitionistic and linear logic, focusing on their use in computer science. The goal is to understand the distinction between classical and constructive logic, define logical connectives, implement theorem provers, and explore computational interpretations of logics. Concepts covered include natural deduction, sequent calculus, logic programming, linear logic, and many more.
No concepts data
+ 35 more concepts