Campus Event Calendar
Event Entry
What and Who
Proof by induction in sequent calculus modulo
Fabrice Nahon
INRIA-LORIA
Talk RG1 Group Meeting
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 8 February 2008
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
We are presenting an original narrowing-based proof search method for
inductive theorems. It has the specificity to be grounded on deduction modulo
and to rely on
narrowing to provide both induction variables and instantiation
schemes. It also yields a direct translation
from a successful proof search derivation to a proof in the sequent
calculus. The method is shown to be correct and refutationally
complete in a proof theoretical way.
We are extending this first approach to equational rewrite theories given by
a rewrite system R and a set E of equalities.
Whenever the equational rewrite system (R,E) has good properties of
termination, sufficient
completeness, and whenever E is constructor preserving, narrowing at
defined-innermost positions is performed with unifiers which are constructor
substitutions. This is especially interesting for associative and
associative-commutative theories for which the general proof search
system is refined.
Keywords: deduction modulo, sequent calculus modulo, induction, Noetherian
induction,
induction by rewriting, equational reasoning, term rewriting, equational
rewriting
equational narrowing.
inductive theorems. It has the specificity to be grounded on deduction modulo
and to rely on
narrowing to provide both induction variables and instantiation
schemes. It also yields a direct translation
from a successful proof search derivation to a proof in the sequent
calculus. The method is shown to be correct and refutationally
complete in a proof theoretical way.
We are extending this first approach to equational rewrite theories given by
a rewrite system R and a set E of equalities.
Whenever the equational rewrite system (R,E) has good properties of
termination, sufficient
completeness, and whenever E is constructor preserving, narrowing at
defined-innermost positions is performed with unifiers which are constructor
substitutions. This is especially interesting for associative and
associative-commutative theories for which the general proof search
system is refined.
Keywords: deduction modulo, sequent calculus modulo, induction, Noetherian
induction,
induction by rewriting, equational reasoning, term rewriting, equational
rewriting
equational narrowing.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 01/23/2008 09:55
Roxane Wetzel, 01/11/2008 12:12
Roxane Wetzel, 11/05/2007 11:19
Roxane Wetzel, 10/24/2007 14:00 -- Created document.
Roxane Wetzel, 01/11/2008 12:12
Roxane Wetzel, 11/05/2007 11:19
Roxane Wetzel, 10/24/2007 14:00 -- Created document.