Correcting Faulty Conjectures by Logic Program Synthesis

Colloque avec actes et comité de lecture. internationale.International audienceIt'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