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.