Series: Logic Seminar
Date: Tuesday, October 5, 1999
Speaker: Dale Miller (Penn State, CSE)
Title: A Meta-Logic for Sequent Calculus, continued
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.