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

Automated mathematical induction

Adel Bouhoula 1 Emmanuel Kounalis Michaël Rusinowitch 1
1 EURECA - Proof, Symbolic Computation and Logic
UHP - Université Henri Poincaré - Nancy 1, CRIN - Centre de Recherche en Informatique de Nancy, INRIA Lorraine
Abstract : Proofs by induction are important in many computer science and artifical intelligence applications, in particular, in program verification and specification systems. We present a new method to prove (and disprove) automatically inductives properties. Given a set of axioms, a well-suited induction scheme is constructed automatically. We call such and induction scheme a test set. Then, for proving a property, we just instantiate it with terms from the test set and apply pure algebraic simplifications to the result. This method needs no completion and explicit induction. However it retains their positive features, namely, the completeness of the former and the robustness of the latter. It has been implemented in the theorem-prover SPIKE.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 4:49:28 PM
Last modification on : Friday, February 4, 2022 - 3:25:31 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 3:58:50 PM


  • HAL Id : inria-00074894, version 1



Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch. Automated mathematical induction. [Research Report] RR-1663, INRIA. 1992. ⟨inria-00074894⟩



Record views


Files downloads