HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:38:45 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00099562, version 1



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



Record views