Automated mathematical induction - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1994

Automated mathematical induction

E. Kounalis
  • Fonction : Auteur
Michaël Rusinowitch

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-2187.pdf (2.06 Mo) Télécharger le fichier

Dates et versions

inria-00074484 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00074484 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More