Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Type-theoretic interpretations of proof search
Date, Time and Location
Abstract
lies at the heart of most efficient proof procedures because the
logic admits least-commitment search. The key to extending such
methods to quantifiers and non-classical connectives is the problem
of recovering this least-commitment principle in the context of the
non-classical/non-propositional logic; i.e., characterizing when a
least-commitment classical search yields sufficient evidence for
provability in the non-classical logic.
As a prelude to studying these embedings in depth, a type-theoretic
interpretation of search in the classical sequent calculus has been
developed based on an extension of Michel Parigot's lambda-mu-calculus
for free deduction. This system provides a type-theoretic view of
the basic system of evidence for any matrix characterisation of a
non-classical logic.
I shall present the system of realisers, prove strong normalisation
properties, and show how to interpret the classical sequent calculus
in it. To illustrate the use of the system for a non-classical logic
I shall show how to characterise provability in intuitionistic logic
using the classical realisers.
This is a report on joint work with Eike Ritter (Birmingham) and David
Pym (Queen Mary and Westfield College, London).
Contact
Tags, Category, Keywords and additional notes
Vortragswuensche fuer das Logikseminar bitte an Uwe Waldmann, MPI,
Tel.: (0681) 9325-227, uni-intern: 92227