A Method for Patching Faulty Conjectures

Moussa Demba 1 Francis Alexandre 2 Khaled Bsaïes 1
2 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Type de document :
Rapport
[Intern report] A04-R-321 || demba04a, 2004, 20 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00100226
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:15:45
Dernière modification le : mardi 24 avril 2018 - 13:36:45

Identifiants

  • HAL Id : inria-00100226, version 1

Collections

Citation

Moussa Demba, Francis Alexandre, Khaled Bsaïes. A Method for Patching Faulty Conjectures. [Intern report] A04-R-321 || demba04a, 2004, 20 p. 〈inria-00100226〉

Partager

Métriques

Consultations de la notice

82