Implicit induction in conditional theories - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1993

Implicit induction in conditional theories

Adel Bouhoula
  • Fonction : Auteur
  • PersonId : 756484
  • IdRef : 132449021
Michaël Rusinowitch

Résumé

We propose a new procedure for proof by induction in conditional theories where case analysis is simulated by term rewriting. This technique reduces considerably the number ofvariables of a conjecture to be considered for applying induction schemes (inductive positions). Our procedure is presented as a set of inference rules whose correctness has been formally proved. Moreover, when the axioms are ground convergent it is possible to apply the system for refuting conjectures. The procedure is even refutationally complete for conditional equations with boolean preconditions over free constructors (under the same hypotheses). The method is entirely implemented in the prover SPIKE. This system has proved interesting examples in a completely automatic way, that is, without interaction with the user and without ad-hoc heuristics. It has also proved the challenging Gilbreath card trick, with only 2 easy lemmas.

Domaines

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

Dates et versions

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

Identifiants

  • HAL Id : inria-00074627 , version 1

Citer

Adel Bouhoula, Michaël Rusinowitch. Implicit induction in conditional theories. [Research Report] RR-2045, INRIA. 1993. ⟨inria-00074627⟩
74 Consultations
94 Téléchargements

Partager

Gmail Facebook X LinkedIn More