### Towards Proof Planning in Logical Frameworks

**Speaker:**
Carsten
Schürmann
**When & Where:** 12:30pm, Wednesday, Sept 25, 2002, Room 400 AKW

**Abstract:**

In many respects reasoning about properties of programming languages,
compilers, types systems, logics, protocol systems, or safety
architectures is a challenging problem. Formulation of theorems is
problematic, finding their proofs is often even more difficult and so
is learning from failure. Can we prove automatically that a logic
used in a proof carrying safety architecture is sound, that a
programming language preserves types, or that an authentication
protocol is safe?

In this talk I will give an introduction to logical frameworks and
describe the results we have achieved by integrating them with
automated theorem proving techniques. One technique that we consider
to be particularly important is proof planning. To this end we have
developed a logically clean and elegant criterion that allows a
theorem prover to recognize unpromising proof states early in a
proof. It is currently being implemented into a theorem for a proof
assistant based on the logical framework LF.