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.