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 :
Theses
Complete list of metadatas

Cited literature [31 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01748604
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:42:50 AM
Last modification on : Tuesday, January 29, 2019 - 1:21:50 AM
Long-term archiving on : Friday, September 14, 2018 - 10:42:41 AM

File

SCD_T_1995_0007_CURIEN.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01748604, version 1

Collections

Citation

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

Share

Metrics

Record views

73

Files downloads

28