Utilisation des schématisations de termes en déduction automatique, Using term schematisations in automated deduction

Hicham Bensaid

Description

Sous la direction de Ricardo Caferra, Nicolas Peltier
Thèse soutenue le 17 juin 2011: Grenoble
Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks.
-Démonstration automatique de théorèmes
-Démonstration automatique de théorèmes
-I-termes
-Analyse de l'espace de recherche
-Complétude réfutationnelle
-Indexation de termes
Term schematisations allow one to represent infinite sets of terms having a similar structure by a finite and compact form. In this work we study some issues related to the use of term schematisation in automated deduction, in particular in saturation-based first-order theorem proving. After a brief comparative study of existing schematisation formalisms, we focus on terms with integer exponents (or I-terms). We first propose a new approach allowing to automatically detect regularities (obviously not always) on search spaces. This is motivated by our aim at extending current theorem provers with qualitative improvements. For instance, detecting regularities permits to discover lemmata which is mandatory for terminating in some kinds of inductive proofs. We present DS3, a tool which implements these ideas. Our approach departs from existing techniques since on one hand it is completely independent of the proof procedure used and on the other hand it uses inductive generalization techniques instead of deductive ones. We discuss advantages and disadvantages of our method and we give some informal elements of comparison with similar approaches. Next we tackle some theoretical aspects of the use of I-terms in automated deduction. We prove that the direct extension of the ordered resolution calculus is refutationally complete. We provide an example showing that a direct extension of the superposition calculus is not refutationally complete and we propose a new inference rule to restore refutational completeness. We then propose an indexing algorithm for (a subclass of) I-terms. This algorithm is an extension of the perfect discrimination trees that are are employed by many efficient theorem provers to implement redundancy elimination rules. Finally we present DEI, a theorem prover with built-in capabilities to handle formulae containing I-terms. This theorem-prover is an extension of the E-prover developed by S. Schulz. We evaluate the performances of this software on a set of benchmarks.
-Automated theorem proving
-Term schematization
-I-termes
-Search space analysis
-Refutation completeness
-Refutation completenessterm indexing
Source: http://www.theses.fr/2011GRENM019/document

Sujets

• Démonstration automatique de théorèmes

Informations

• Publié par: Thesee
• Nombre de lectures: 77
• Langue: Français
• Poids de l'ouvrage: 2 Mo

Extrait

THÈSE
Pour obtenir le grade de
DOCTEURDEL’UNIVERSITÉDEGRENOBLE
Spécialité :Informatique
Arrêté ministériel : 7 août 2006
Présentée par
HichamBENSAID
Thèse dirigée parRicardoCAFERRA etNicolasPELTIER
préparée au sein duLaboratoired’InformatiquedeGrenoble
et de l’École Doctorale Mathématiques, Sciences et Technologies de
l’Information,Informatique
UTILISATIONDESSCHÉMATISATIONS
DE TERMES EN DÉDUCTION AUTO-
MATIQUE
Thèse soutenue publiquement le17juin2011,
devant le jury composé de :
DominiqueDUVAL
Professeure à l’Université Joseph Fourier, Présidente
DenisLUGIEZ
Professeur à l’Université de Provence, Rapporteur
ChristopherLYNCH
Professeur à la Clarkson University, Rapporteur
BernhardGRAMLICH
Associate Professor à la Technische Universität Wien, Examinateur
RicardoCAFERRA
Maître de conférences (HDR) à l’ENSIMAG, Directeur de thèse
NicolasPELTIER
Chargé de recherche (HDR) au CNRS, Directeur de thèse
tel-00618531, version 1 - 2 Sep 2011tel-00618531, version 1 - 2 Sep 2011J’en viens à ceci, que les travaux d’écolier sont des épreuves
pour le caractère, et non point pour l’intelligence. Que ce soit
orthographe, version ou calcul, il s’agit de surmonter l’humeur,
il s’agit d’apprendre à vouloir.
Émile-Auguste Chartier, dit Alain
Propos sur l’éducation
tel-00618531, version 1 - 2 Sep 2011tel-00618531, version 1 - 2 Sep 2011Résumé
Les schématisations de termes permettent de représenter des ensembles infinis de termes
ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions cer-
tains aspects liés à l’utilisation des schématisations de termes en déduction automatique, plus
particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par satu-
ration.
Après une brève étude comparée des formalismes de schématisation existants, nous nous
concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un
premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement
des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs
applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines
preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons
notre approche avec d’autres techniques de généralisation de termes. Notre approche diffère com-
plètement des techniques existantes car d’une part, elle est complètement indépendante de la pro-
cédure de preuve utilisée et d’autre part, elle utilise des techniques de généralisation inductive et
non déductives. Nous discutons également les avantages et les inconvénients liés à l’utilisation de
notre méthode et donnons des élements informels de comparaison avec les approches existantes.
Nous nous intéressons ensuite aux aspects théoriques de l’utilisation des I-termes en dé-
monstration automatique. Nous démontrons que l’extension auxI-termes du calcul de résolution
ordonnée est réfutationnellement complète, que du calcul de superposition n’est pas
réfutationnellement complète et nous proposons une nouvelle règle d’inférence pour restaurer la
complétude réfutationnelle.
Nous proposons ensuite un algorithme d’indexation (pour une sous-classe) desI-termes, utile
pour le traitement des règles de simplification et d’élimination de la redondance.
Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de
gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce
logiciel sur un ensemble de benchmarks.
Mots clés : démonstrationautomatiquedethéorèmes,schématisationdetermes,I-termes,ana-
lyse de l’espace de recherche, complétude réfutationnelle, indexation de termes.
i
tel-00618531, version 1 - 2 Sep 2011Abstract
Term schematisations allow one to represent infinite sets of terms having a similar structure
by a finite and compact form. In this work we study some issues related to the use of term
schematisation in automated deduction, in particular in saturation-based first-order theorem
proving.
After a brief comparative study of existing schematisation formalisms, we focus on terms with
integer exponents (orI-terms). We first propose a new approach allowing to automatically detect
regularities (obviously not always) on search spaces. This is motivated by our aim at extending
current theorem provers with qualitative improvements. For instance, detecting regularities
permits to discover lemmata which is mandatory for terminating in some kinds of inductive
proofs. We present DS3, a tool which implements these ideas. Our approach departs from
existing techniques since on one hand it is completely independent of the proof procedure used
and on the other hand it uses inductive generalization techniques instead of deductive ones.
We discuss advantages and disadvantages of our method and we give some informal elements of
comparison with similar approaches.
Next we tackle some theoretical aspects of the use of I-terms in automated deduction. We
prove that the direct extension of the ordered resolution calculus is refutationally complete.
We provide an example showing that a direct extension of the superposition calculus is not
refutationally complete and we propose a new inference rule to restore refutational completeness.
We then propose an indexing algorithm for (a subclass of) I-terms. This algorithm is an
extension of the perfect discrimination trees that are are employed by many efficient theorem
provers to implement redundancy elimination rules.
Finally we present DEI, a theorem prover with built-in capabilities to handle formulae con-
taining I-terms. This theorem-prover is an extension of the E-prover developed by S. Schulz.
We evaluate the performances of this software on a set of benchmarks.
Keywords: automated theorem proving, term schematisation, I-termes, search space analysis,
refutation completeness, term indexing.
ii
tel-00618531, version 1 - 2 Sep 2011Remerciements
Je tiens en premier à remercier vivement tous les membres du jury qui m’ont fait l’honneur
d’évaluer ce travail et d’y apporter de leur notoriété. Ainsi, je remercie Dominique Duval Pro-
fesseure à l’Université Joseph Fourier d’avoir bien voulu présider le jury. Je remercie également
Denis Lugiez professeur à l’Université de Provence et Christopher Lynch Professeur à la Clarkson
University d’avoir bien voulu accepter la lourde tâche de rapporter cette thèse. Mes remercie-
ments s’adressent aussi à Bernhard Gramlich Associate Professor à la Technische Universität
Wien pour avoir bien voulu faire partie du jury et évaluer ce travail.
À tout seigneur tout honneur. Je tiens à exprimer ma gratitude la plus profonde à Ricardo
Caferra et Nicolas Peltier, mes directeurs de thèse pour leur amitié, pour leur sympathie, pour
leurs valeurs humaines, pour leur disponibilité, pour leur implication totale dans ce travail, pour
leur aide et leur soutien illimités même durant les moments les plus difficiles, pour leurs lectures
minutieuses et leurs corrections répétées des différentes versions intermédiaires de ce manuscrit,
enfin pour tout ce qu’ils ont fait pour moi. Qu’ils puissent trouver dans ces quelques lignes
l’expression de mon admiration et de ma reconnaissance les plus profondes.
Une pensée particulière à l’Institut National des Postes et Télécommunications de Rabat qui
m’a offert le cadre et les moyens pour un bon déroulement de cette thèse.
Enfin, je tiens à remercier chaleureusement ma famille et mes amis pour leurs encouragements
et leur soutien durant ces années de thèse.
iii
tel-00618531, version 1 - 2 Sep 2011iv
tel-00618531, version 1 - 2 Sep 2011Table des matières
1 Introduction 1
I Définitions 5
2 Préliminaires 7
2.1 Termes du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.1.2 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.2 Démonstration automatique et saturation . . . . . . . . . . . . . . . . . . . . . . 11
2.2.1 Cas non équationnel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.2 Cas équationnel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.2.3 Élimination de la redondance et saturation . . . . . . . . . . . . . . . . . 17
2.3 Preuves inductives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3 Schématisation de termes 21
3.1 Définitions préliminaires . . . . . . . . . . . . . . .