Nous présentons une méthode originale de recherche de preuve par récurrence utilisant la surréduction. Elle a la particularité d'être fondée sur la déduction modulo et d'utiliser la surréduction pour sélectionner à la fois les variables de récurrence et les schémas d'instanciation. Elle donne également la possibilité de traduire directement toute dérivation effectuée avec succès en une preuve dans le calcul des séquents modulo. La correction et la complétude réfutationnelle de la méthode sont démontrées en théorie de la preuve. Nous étendons ensuite cette première approche aux théories de réécriture équationnelles constituées d'un système de réécriture R et d'un ensemble E d'égalités. A partir du moment où le système de réécriture équationnel (R,E) possède de bonnes propriétés de terminaison et de complétude suffisante, et si on suppose également que E préserve les constructeurs, la surréduction au niveau des positions les plus profondes où apparaît un symbole défini s'effectue uniquement à l'aide d'unificateurs qui sont également des substitutions constructeurs. Ceci est particulièrement intéressant dans le cas des théories associatives, ou associatives commutatives, pour lesquelles notre système de recherche de preuve a été raffiné.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00259803 |
| Date | 25 October 2007 |
| Creators | Nahon, Fabrice |
| Publisher | Université Henri Poincaré - Nancy I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds