Correction de conjectures faussses - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2002

Correction de conjectures faussses

Résumé

Dans le domaine de la vérification, les preuves se terminent souvent par des formules fausses ou non prouvables. En général, le prouveur signale simplement l'échec. Cependant, dans certains cas il est intéressant de connaître la cause de cet échec et de le corriger. Les méthodes de preuves classiques sont insuffisantes pour qu'un prouveur détecte et corrige automatiquement les erreurs dans les programmes ou formules. Dans cet article, nous proposons une méthode permettant de corriger des conjectures fausses. Soit $\forall x~\Phi(x)$ une conjecture partiellement fausse, la méthode proposée consiste à construire un prédicat de correction P tel que $\forall x~(P(x)\Rightarrow \Phi(x))$ soit valide.
Fichier non déposé

Dates et versions

inria-00101078 , version 1 (26-09-2006)

Identifiants

  • HAL Id : inria-00101078 , version 1

Citer

Moussa Demba, Francis Alexandre, Khaled Bsaïes. Correction de conjectures faussses. [Interne] A02-R-492 || demba02a, 2002. ⟨inria-00101078⟩
61 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More