Series: Logic Seminar Speaker: Dale Miller, Computer Science and Engineering, Penn State Title: Sequent Calculus and the Specification of Computation Date: Tuesday, March 17, 1998, 2:30 PM Location: 308 Boucke Building Abstract: In recent years, sequent calculus presentations of proof systems have been used in a number of applications of logic to computer science. In this lecture, I will show how sequent calculus can be used to define logic programming as ``goal-directed search'' of cut-free sequent proofs. From such a foundation, various logic programming languages have been designed that exploit subsets of classical, intuitionistic, and linear logic. Given their foundation in logic and proof theory, novel ways to reason about logic programs are also possible. I will introduce the sequent calculus and show how it can be used to specify and reason about various kinds of computations.
Mathematical Logic at Penn State
Department of Mathematics