Title and Abstract for an Invited Talk at the
15th International Conference on Automated Deduction (CADE-15),
Lindau, Germany, July 5-10, 1998
--------------------------------------------------

Reasoning About Deductions in Linear Logic

Frank Pfenning
Carnegie Mellon University


Linear logic has been described as a logic of state.  Many complex
systems involving state transitions, such as imperative programming
languages, concurrent systems, protocols, planning problems, games, or
abstract machines, can be specified in linear logic at a very high level
of abstraction.  Generally, these encodings represent legal sequences of
transitions as deductions in linear logic.

Proof search in linear logic then allows us to establish the existence
of transition sequences, thereby, for example, solving a planning
problem or modelling the execution of a protocol.  But we often need to
consider all possible computations, for example, to establish that an
imperative programming language is type-safe or that a protocol is
secure.  This then requires reasoning about deductions in linear logic.

We describe our approach to proving properties of deductions in linear
logic which is based on a linear logical framework (LLF) and an explicit
meta-logic with universal and existential quantifiers ranging over proof
objects.  Due to the immediacy of the encodings, the expressive power of
the linear logical framework, and the design of the meta-logic this
architecture offers excellent opportunities for automation, combining
techniques from type theory, constraint logic programming, and inductive
theorem proving.

Preliminary results with a non-linear prototype have been very
encouraging and include, for example, automatic proofs of Hilbert's
deduction theorem, type preservation for mini-ML, and soundness and
completeness of logic programming search.

[The talk presents joint work with Iliano Cervesato, Stanford University,
 and Carsten Schuermann, Carnegie Mellon University]