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.