Series: Logic Seminar

Date: Tuesday, September 28, 1999

Speaker: Dale Miller (Penn State, CSE)

Title: A Meta-Logic for Sequent Calculus

Time: 2:30 - 3:20 PM

Place: 122 Thomas Building

Abstract: 

Linear logic can be used as a meta-logic to specify a variety of
sequent calculus proof systems for classical, intuitionistic, and
linear logic. The specification of inference rules translates
naturally to certain linear logic programming clauses. The operational
semantics of linear logic arising from goal-directed search translates
directly into object-level proof search semantics. Girard's Logic of
Unity (LU) can be motivated and specified naturally using this
meta-logic approach. Finally, we show how the meta-theory of linear
logic can be used to prove various properties of object-level proof
systems.