Correcting Faulty Conjectures by Logic Program Synthesis

Moussa Demba Khaled Bsaïes Francis Alexandre 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : It's highlighted that when proving conjectures or synthesising programs, we are sometimes faced with an unprovable conjecture. In general, a theorem prover will do nothing more but indicates the conjecture is false. However, in many cases it is highly desirable to have an automated means for detecting and correcting faulty conjectures. Classical methods are not able to detect automatically unconsistancy in conjectures. In this paper, we present a method for patching faulty conjectures. Let $\Phi$ be a faulty conjecture, the proposed method builds a definition for a corrective predicate P such that $\forall x~(\Phi(x)\Leftarrow P(x))$ is a theorem.
Type de document :
Communication dans un congrès
International Conference on Computers Systems and Applications 2003 - AICCSA'03, 2003, Tunis, Tunisie, 6 p, 2003
Liste complète des métadonnées

https://hal.inria.fr/inria-00099562
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:38:45
Dernière modification le : mardi 24 avril 2018 - 13:34:49

Identifiants

  • HAL Id : inria-00099562, version 1

Collections

Citation

Moussa Demba, Khaled Bsaïes, Francis Alexandre. Correcting Faulty Conjectures by Logic Program Synthesis. International Conference on Computers Systems and Applications 2003 - AICCSA'03, 2003, Tunis, Tunisie, 6 p, 2003. 〈inria-00099562〉

Partager

Métriques

Consultations de la notice

41