CPSC 629: Deductive Systems
Instructor: Carsten Schürmann
Department of Computer Science
Yale University
Time: TTh 4:00-5:15
Room: AKW 500
|
|
Home |
|
|
Schedule |
|
|
Handouts |
|
|
Assignments |
|
|
Projects |
|
|
Links |
Lecture 15: Sequent Calculus
In this lecture we discuss another formal system for first order logic: The sequent calculus which is due to Gentzen 1934. After encoding natural deduction derivations and sequent derivations in LF we prove that the former can be embedded into the latter.
Suggested Reading Materials:
Frank Pfenning. Sequent Calculus
Previous lecture: Lecture 14Next lecture: Lecture 16