Double-negation translation is a method used in proof theory to embed classical logic into intuitionistic logic. It involves translating formulas to equivalent ones that are not equivalent in intuitionistic logic. This approach has been applied in various instances, such as Glivenko's translation for propositional logic and the Gödel-Gentzen and Kuroda translations for first-order logic.
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