Campus Event Calendar

Event Entry

What and Who

Towards Proof Automation in Logical Frameworks

Carsten Schuermann
Yale University
AG 1, AG 2, AG 3, AG 4  
Expert Audience

Date, Time and Location

Tuesday, 17 December 2002
-- Not specified --
46.1 - MPII


Carsten Schürmann (Yale University):
Towards Proof Automation in Logical Frameworks
(joint work with Serge Autexier)


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 the recognition of
none-theorems. To this end we have developed a logically clean
and elegant criterion that prevents our theorem prover from
exploring unnecessary branches in the search state. The theorem
prover is currently being implemented into a proof assistant
based on the logical framework LF.


--email hidden
passcode not visible
logged in users only