Campus Event Calendar
Event Entry
What and Who
Good proofs in deduction modulo
Guillaume Burel
INRIA, Nancy
Talk
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 12 June 2009
11:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
We study how to integrate theories into a deductive system to simplify
mechanized proof search in those theories. We are particularly
interested in deduction modulo and superdeduction, two close formalisms
allowing the integration of computations into proofs through a rewrite
system. We consider three simplicity criteria related to proof search.
Cut admissibility makes it possible to restrain the proof-search space
but does not always hold in deduction modulo. We define a completion
method transforming a rewrite system representing computations so that
at the end cut admissibility holds. By the way, we show how to
transform any first-order theory into a rewrite system that can be used
in deduction modulo.
We show then how deduction modulo unboundedly reduces proof lengths,
by transferring deduction steps into computations. In particular, we
apply this to higher-order arithmetic to show that proof-length
speedups between ith- and i+1st-order arithmetic disappear when
working in deduction modulo, making it possible to work in first-order
logic modulo without increasing proof lengths.
Following this last result, we investigate which higher-order systems
can be simulated in first order using deduction modulo, and more
generally how deduction modulo and superdeduction can be used as logical
frameworks. In particular, we show that all functional pure type
systems, which are generic type systems for the lambda-calculus with
dependent types, can be encoded in superdeduction.
mechanized proof search in those theories. We are particularly
interested in deduction modulo and superdeduction, two close formalisms
allowing the integration of computations into proofs through a rewrite
system. We consider three simplicity criteria related to proof search.
Cut admissibility makes it possible to restrain the proof-search space
but does not always hold in deduction modulo. We define a completion
method transforming a rewrite system representing computations so that
at the end cut admissibility holds. By the way, we show how to
transform any first-order theory into a rewrite system that can be used
in deduction modulo.
We show then how deduction modulo unboundedly reduces proof lengths,
by transferring deduction steps into computations. In particular, we
apply this to higher-order arithmetic to show that proof-length
speedups between ith- and i+1st-order arithmetic disappear when
working in deduction modulo, making it possible to work in first-order
logic modulo without increasing proof lengths.
Following this last result, we investigate which higher-order systems
can be simulated in first order using deduction modulo, and more
generally how deduction modulo and superdeduction can be used as logical
frameworks. In particular, we show that all functional pure type
systems, which are generic type systems for the lambda-calculus with
dependent types, can be encoded in superdeduction.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 06/09/2009 10:29 -- Created document.