Skip to Main content Skip to Navigation

Outils pour la preuve par analogie

Abstract : This thesis aims at producing tools for automated deduction in order to reuse established results: proof by analogy consists in building new proofs from existing ones. We first have to recognize the similarity between an already solved problem and the current one. Then, we transform the existing solution to obtain a solution for the new problem. The aim of our approach is to formally define relations between first order logical formulas - the one for which we have a proof is called a reference - in order to deduce an automatic transformation of the reference proof into a proof of the new formula. The analogy concept is very powerful, but also very intuitive. Therefore, we have reduced it to simpler concepts to enable their automation. We have defined four relations on formulas that we call similarities. These relations take into account propositional logic properties, quantifier properties, function and predicate renaming, and the connectors Associative-Commutative properties. A fundamental tool for recognizing similarities between formulas is a second-order AC-matching algorithm. The completeness and termination of this algorithm show the decidability of the second-order AC-matching problem. Relative proof transformations are given for expansion-tree proofs, introduced by Miller and Pfenning: this representation has sorne relevant properties for analogy. In order to go beyond the similarity stage, we introduce the difference calcul us, which uses matching failures. We show that when the difference between formulas is simple, we may hope for a complete analogy process. Finally, we show, in a general setting and using examples, how analogy can be viewed by studying differences.
Document type :
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 11:42:50 AM
Last modification on : Wednesday, May 4, 2022 - 11:02:18 AM
Long-term archiving on: : Friday, September 14, 2018 - 10:42:41 AM


Files produced by the author(s)


  • HAL Id : tel-01748604, version 1



Régis Curien. Outils pour la preuve par analogie. Informatique [cs]. Université Henri Poincaré - Nancy 1, 1995. Français. ⟨NNT : 1995NAN10007⟩. ⟨tel-01748604⟩



Record views


Files downloads