Incorporating Decision Procedures in Implicit Induction |
| |
Affiliation: | 1. DIST, Università di Genova, Viale Causa 13, 16145 Genova, Italy;2. LORIA-INRIA, 615, rue du Jardin Botanique, 54602 Villers lès Nancy, France;3. INRIA, 2004 route des Lucioles, BP 93, 06902 Sophia Antipolis, France |
| |
Abstract: | In this paper we present an approach to integrating reasoning specialists into cover set induction based on constraint contextual rewriting. The approach has been successfully used to incorporate decision procedures into theSPIKE prover. Computer experiments on non-trivial verification problems illustrating the effectiveness of the proposed technique are given. The generality of the approach allows for the integration of computer algebra algorithms and techniques into induction theorem provers. To illustrate this, we discuss the integration of the Buchberger algorithm into our framework. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|