Correcting faulty conjectures by logic program synthesis

Summary form only given. We highlight that when proving conjectures or synthesising programs, we are sometimes faced with improvable conjectures. In general, a theorem prover will do nothing more than indicate 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 automatically detect unconsistancy in conjectures. We present a method for patching faulty conjectures. Let /spl phi/ be a faulty conjecture, the proposed method builds a definition for a corrective predicate P such that /spl forall/x (/spl phi/(x) /spl lArr/ P(x)) is a theorem.