Skip to Main content Skip to Navigation
Reports

Automated mathematical induction

Adel Bouhoula 1 E. Kounalis Michaël Rusinowitch
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Proofs by induction are important in many computer science and artificial intelligence applications, in particular, in program verification and specification systems. We present a new method to prove (and disprove) automatically inductive properties. Given a set of axioms, a well-suited induction scheme is construted automatically. We call such an induction scheme a test set. Then, for proving a property, we just instantiate it with terms from the test set and apply pure algebraic simplification 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 :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00074484
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 3:24:34 PM
Last modification on : Wednesday, January 8, 2020 - 2:16:59 PM
Long-term archiving on: : Tuesday, April 12, 2011 - 5:08:41 PM

Identifiers

  • HAL Id : inria-00074484, version 1

Collections

Citation

Adel Bouhoula, E. Kounalis, Michaël Rusinowitch. Automated mathematical induction. [Research Report] RR-2187, INRIA. 1994, pp.42. ⟨inria-00074484⟩

Share

Metrics

Record views

268

Files downloads

161