Fall 2021

Carnegie Mellon University

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.

This undergraduate course provides an introduction to constructive logics, such as intuitionistic and linear logic, with an emphasis on their application in computer science. This includes basic means for defining logics (for example, natural deduction and sequent calculus), establishing properties of logics (for example, cut elimination), and for investigating their computational interpretations (for example, via proof reduction or proof search).

No data.

After taking this course, students should be able to

- understand the distinction between classical and constructive logic, and the uses of constructive logic
- define logical connectives and test these definitions for harmony
- express and prove the relationships between different representations of a logic (e.g., natural deduction and sequent calculus), and explain what each representation is for
- implement propositional theorem provers
- use operational interpretations of logics via proof search (a.k.a. logic programming)
- understand the applications of substructural logics

No data

AdmissibilityBackward ChainingCertifying Theorem ProversClassical LogicCut EliminationDepth estimationDerivabilityFocusingForward ChainingHarmonyHeyting ArithmeticInversionKolmogorov translationLax logic Linear LogicLinear logic applicationsLogic ProgrammingModal LogicMonadsNatural DeductionOrdered LogicOrdered Proofs as Concurrent ProgramsPractical PrologPrologProlog in PrologProofs as ML programsProofs as ProgramsProoftreePropositional Theorem ProvingQuantificationSequent CalculusSession TypesSubsingleton LogicVerificationsVerifications and Uses