Induction using term orders |
| |
Authors: | Francois Bronsard Uday S. Reddy Robert W. Hasker |
| |
Affiliation: | (1) CRIN-INRIA-Lorraine, Nancy, France;(2) Present address: Andersen Consulting, 3773 Willow road, #2f5d, 60062-6212 Northbrook, IL, U.S.A.;(3) The University of Illinois at Urbana-Champaign, U.S.A.;(4) The University of Illinois at Urbana-Champaign, U.S.A. |
| |
Abstract: | We present a procedure for proving inductive theorems which is based on explicit induction, yet supports mutual induction. Mutual induction allows the postulation of lemmas whose proofs use the theorems ex hypothesi while the theorems themselves use the lemmas. This feature has always been supported by induction procedures based on Knuth-Bendix completion, but these procedures are limited by the use of rewriting (or rewriting-like) inferences. Our procedure avoids this limitation by making explicit the implicit induction realized by these procedures. As a result, arbitrary deduction mechanisms can be used while still allowing mutual induction. A preliminary version of this paper appeared in the proceedings of the 12th Conference on Automated Deduction, A. Bundy, editor. This author was supported by a grant from the Ministère des Affaires Etrangères, France. |
| |
Keywords: | Mutual induction automated theorem proving |
本文献已被 SpringerLink 等数据库收录! |
|