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

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

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

Share

Metrics

Record views

76