Loading...
Please wait, while we are loading the content...
Similar Documents
Inductive Proof Search Modulo
| Content Provider | Hyper Articles en Ligne (HAL) |
|---|---|
| Author | Nahon, Fabrice Kirchner, Claude Kirchner, Hélène |
| Copyright Year | 2007 |
| Abstract | We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system R 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 R,E 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 refutationaly complete. |
| Related Links | https://inria.hal.science/inria-00187458/file/ftp-07.pdf |
| Volume Number | Technical report ULCS-07-018 Department of Computer Science University of Liverpool |
| Part | partment |
| Conference Proceedings | 6th International Workshop on First-Order Theorem Proving - FTP 2007 |
| Language | English |
| Publisher | HAL CCSD |
| Publisher Date | 2007-01-01 |
| Access Restriction | Open |
| Subject Keyword | equational rewriting Deduction modulo noetherian induction equational narrowing |
| Content Type | Text |
| Resource Type | Conference Proceedings |
| Subject | Computer Science |
