Sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology. It is one of several extant styles of proof calculus for expressing line-by-line logical arguments, and has significant practical and theoretical advantages compared to Hilbert-style systems. Natural deduction and sequent calculus systems facilitate the elimination and introduction of universal and existential quantifiers so that unquantified logical expressions can be manipulated according to the much simpler rules of propositional calculus.
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 conceptsCarnegie Mellon University
Spring 2022
This course is about software verification, with the goal of writing bug-free code. Students will learn to formalize program correctness, write verified code, and use automated tools for verification. It explores the principles behind verification tools, logical specifications, and deductive reasoning. Previous knowledge in program correctness reasoning is beneficial.
No concepts data
+ 22 more concepts