Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00101078
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:55:51 PM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM

Identifiers

  • HAL Id : inria-00101078, version 1

Collections

Citation

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

Share

Metrics

Record views

89