Inductive proof search modulo

We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiati...

Full description

Saved in:
Bibliographic Details
Published in:Annals of mathematics and artificial intelligence 2009-02, Vol.55 (1-2), p.123-154
Main Authors: Nahon, Fabrice, Kirchner, Claude, Kirchner, Hélène, Brauner, Paul
Format: Article
Language:English
Subjects:
Artificial Intelligence
Complex Systems
Computer Science
Construction
Deduction
Expert systems
Logic in Computer Science
Mathematical analysis
Mathematical models
Mathematics
Proving
Search methods
Searching
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.
ISSN:1012-2443
1573-7470
DOI:10.1007/s10472-009-9154-5