Tools for proof by analogy
Outils pour la preuve par analogie
Résumé
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.
Le but de cette thèse est de fournir des outils permettant à la déduction automatique de réutiliser les résultats déjà obtenus. En effet, la preuve par analogie consiste à construire de nouvelles preuves à partir de preuves existantes. Il faut dans un premier temps reconnaître que le problème à résoudre est semblable à un problème déjà résolu, puis, transformer la solution existante, pour obtenir une solution du nouveau problème. L'approche adoptée consiste à définir formellement des relations liant deux formules logiques du premier ordre - celle dont nous possédons une preuve est appelée référence - pour en déduire une méthode automatique de transformation de la preuve de référence en une preuve de la nouvelle formule. Le concept d'analogie est très puissant, mais aussi très intuitif. Ainsi, pour le formaliser, nous l'avons réduit à des concepts plus simples afin de les automatiser. Nous avons défini quatre relations liant les formules, que nous appelons similitudes. Ces similitudes considèrent les propriétés de la logique propositionnelle, les propriétés des quantificateurs, le renommage des fonctions et prédicats et les propriétés associatives-commutatives des connecteurs logiques. Un outil fondamental pour la reconnaissance de ces similitudes est un algorithme de filtrage du second ordre modulo AC. La complétude et la terminaison de cet algorithme montrent la décidabilité du problème de filtrage AC du second ordre. Les transformations de preuves correspondant à ces similitudes sont données pour les preuves par expansion introduites par Miller et Pfenning. Cette représentation possède des propriétés très intéressantes pour l'analogie. Pour dépasser le stade des similitudes, nous utilisons le calcul de différence, qui utilise les échecs du filtrage. Nous montrons que lorsque la différence entre les deux formules considérées est simple, nous pouvons espérer une méthode complète d'analogie. Enfin, nous montrons, dans le cas général, et à partir d'exemples, comment l'analogie peut être envisagée par l'étude de la différence.
Domaines
Informatique [cs]| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
Loading...