3531 articles – 5253 Notices  [english version]

inria-00100226, version 1

## A Method for Patching Faulty Conjectures

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

N° A04-R-321 || demba04a (2004)

Résumé : We present a method for patching faulty conjectures in automatic theorem proving. The method is based on well-known folding/unfolding deduction rules. 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 –  FACULTE DES SCIENCES DE TUNIS
• 1 :  Faculté des Sciences de Tunis (FST)
• Faculté des Sciences de Tunis
• 2 :  DEDALE (LORIA)
• INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
• Domaine : Informatique/Autre
• Mots-clés : abduction – corrective predicate – implicative formula || abduction – prédicat de correction – formule implicative
• Référence interne : A04-R-321 || demba04a
• Commentaire : Rapport interne.

• inria-00100226, version 1
• oai:hal.inria.fr:inria-00100226
• Contributeur :
• Soumis le : Mardi 26 Septembre 2006, 10:15:45
• Dernière modification le : Jeudi 28 Septembre 2006, 15:22:47