Correction de conjectures faussses

Moussa Demba 1 Francis Alexandre 2 Khaled Bsaïes 1
2 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Rapport
[Interne] A02-R-492 || demba02a, 2002
Liste complète des métadonnées

https://hal.inria.fr/inria-00101078
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:55:51
Dernière modification le : jeudi 11 janvier 2018 - 06:20:08

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

69