3543 articles – 5273 references  [version française]

inria-00100052, version 1

## Predicate Synthesis from Inductive Proof Attempt of Faulty Conjectures

Francis Alexandre () a1, Khaled Bsaïes b2, Moussa Demba b2

Logic Based Program Synthesis and Transformation: 13th International Symposium - LOPSTR 2003 3018 (2003) 20-33

Abstract: We present a method for patching faulty conjectures in automatic theorem proving. The conjectures we are interested in here are implicative formulas that are of the following form\,: $\forall \overline{ x}~\phi( \overline{ x})=\forall \overline{x} ~\exists \overline{Y} ~\Gamma(\overline{x},\overline{Y}) \leftarrow \Delta(\overline{x})$. A faulty conjecture is a statement $\forall \overline{ x}~\phi( \overline{ x})$, which is not provable in some given program ${\cal T}$, defining all the predicates occurring in $\phi$, i.e, ${\cal M(T)}\not \models \forall \overline{ x}~ \phi( \overline{ x})$, where ${\cal M(T)}$ means the least Herbrand model of ${\cal T}$, but it would be if enough conditions, say $P$, were assumed to hold, i.e., ${\cal M(T\cup P)}\models \forall \overline{ x}~ \phi( \overline{ x})\leftarrow P$, where ${\cal P}$ is the definition of $P$. The missing hypothesis $P$ is called a corrective predicate for $\phi$. To construct $P$, we use the abduction mechanism that is the process of hypothesis formation. In this paper, we use the logic based approach because it is suitable for the application of deductive rules.

• a –  UNIVERSITE HENRI POINCARE
• b –  FACULTE DES SCIENCES DE TUNIS
• 1:  DEDALE (LORIA)
• INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
• 2:  Faculté des Sciences de Tunis (FST)
• Faculté des Sciences de Tunis
• Domain : Computer Science/Other
• Keywords : program synthesis – theorem proving – abduction – corrective predicate || synthèse de programme – preuve – prédicat de correction
• Internal note : A04-R-320 || alexandre04c
• Comment : LOPSTR'2003 - Revised Selected Papers. Colloque avec actes et comité de lecture. nationale.

• inria-00100052, version 1
• oai:hal.inria.fr:inria-00100052
• From:
• Submitted on: Tuesday, 26 September 2006 10:13:44
• Updated on: Thursday, 28 September 2006 15:22:47