HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information

# Correcting Faulty Conjectures by Logic Program Synthesis

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.
Keywords :
Document type :
Conference papers
Domain :

https://hal.inria.fr/inria-00099562
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

### Identifiers

• HAL Id : inria-00099562, version 1

### 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, ACS, IEEE, 2003, Tunis, Tunisie, 6 p. ⟨inria-00099562⟩

Record views