HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

A General Framework to Build Contextual Cover Set Induction Provers

Sorin Stratulat 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Cover set induction is known as a proof method that keeps the advantages of explicit induction and proof by consistency. Most implicit induction proof procedures are defined in a cover set induction framework. \emph{Contextual cover set} is a new concept that fully characterizes explicit induction schemes, such as the cover sets, and simplification techniques specific to the `proof by consistency' approach. Firstly, we present an abstract inference system \emph{uniformly} defined in terms of contextual cover sets as our general framework to build implicit induction provers. Then, we show that it generalizes existing cover set induction procedures. This paper also contributes to the general problem of assembling reasoning systems in a sound manner. Elementary contextual cover sets are generated by reasoning modules that implement various simplification techniques defined for a large class of deduction mechanisms such as rewriting, conditional rewriting or resolution-based methods for clauses. We present a generic and sound integration schema of reasoning modules inside our procedure together with a simple methodology for improvements and incremental sound extensions of the concrete proof procedures. As a case study, the inference system of the \spike{} theorem prover has been shown to be an instance of the abstract inference system integrating reasoning modules based on rewriting techniques defined for conditional theories. Our framework allows for \emph{modular} and \emph{incremental} sound extensions of \spike{} when new reasoning techniques are proposed. An extension of the prover, incorporating inductive semantic subsumption techniques, has proved the correctness of the MJRTY algorithm by performing a combination of arithmetic and inductive reasoning.
Document type :
Journal articles
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:52:57 PM
Last modification on : Friday, February 4, 2022 - 3:30:42 AM


  • HAL Id : inria-00100927, version 1



Sorin Stratulat. A General Framework to Build Contextual Cover Set Induction Provers. Journal of Symbolic Computation, Elsevier, 2001, 32 (4), pp.403-445. ⟨inria-00100927⟩



Record views