Sommaire
Sujet
J'ai débuté ma thèse en décembre 1995 sous la direction de Jean-Jacques Chabrier, à mon retour du service national. Le sujet portait sur la résolution de problèmes du calcul des prédicats par une méthode basée sur des techniques CSP. J'ai soutenu ma thèse le 5 Janvier 1999 à Dijon.
Une approche de résolution de problèmes en logique des prédicats fondée sur des techniques de satisfaction de contraintes
mots clés : Calcul des prédicats, Problèmes de Satisfaction de Contraintes (CSP), Démonstration Automatique
Publications
- Thèse
- Sacre : a Constraint Satisfaction Based Theorem Prover,
Proceedings of AAAI-99, Orlando FL, USA, July 99. - Une approche de Résolution de Problèmes en logique fondée sur des Techniques de Satisfaction de Contraintes,
Actes de JFPLC'97, Sixièmes Journées Francophones de Programmation
Logique et Programmation par Contraintes 26-28 Mai 1997,Orléans, France (Postscript)
Résumé
La Démonstration Automatique est un domaine de recherche qui s'est fixé pour objectif la résolution, par des mécanismes d'inférence de problèmes exprimés en logique. La vaste gamme des problèmes traités en démonstration automatique, s'étend des problèmes simples, du genre casse-tête, aux problèmes difficiles que sont la démonstration de théorèmes en mathématiques ou la conception de circuits électroniques logiques.
Dans cette thèse, nous définissons un nouveau cadre de travail pour la résolution des problèmes de la logique des prédicats, spécifiés sous forme normale conjonctive. Ce cadre de travail s'établit sur base d'une modélisation des problèmes traités, sous forme de Problèmes de Satisfaction de Contraintes (CSP). D'autre part, nous cherchons à adapter les techniques de résolution des CSP aux problèmes ainsi obtenus. Cette intrusion du formalisme des CSP, à l'intérieur d'un cadre logique, ne revêvet pas seulement un caractère technique, mais sous-tend l'utilisation de procédés qui ont montré leur capacité à résoudre efficacement les problèmes du calcul propositionnel. Notre contribution consiste à élever ces techniques à l'ordre supérieur, c'est-à-dire, en calcul des prédicats, et à montrer la similitude existant entre l'approche logique et l'approche problèmes de satisfaction de contraintes.
L'objectif de ces travaux vise à concevoir un logiciel baptisé SACRE (pour SAtisfaction de Contraintes et REsolution) réalisant l'implantation de la méthode dégagée par notre approche, ainsi qu'à développer une interface graphique utilisateur permettant de réaliser facilement des expérimentations poussées sur un panel de problèmes considérés comme une mesure de référence des démonstrateurs automatiques.
Résultats
La table suivante présente les résultats comparatifs (temps en secondes) entre :
- Otter 3.0.4 en mode auto
- Setheo (meilleur résultat entre -dr ou -wdr)
- Sacre en mode auto
| Problem | Otter | Setheo | Sacre |
| BOO006-1 | 3 | 0 | 0 |
| BOO012-1 | 8 | 0 | 0 |
| BOO016-1 | 2 | 11 | 1 |
| CAT003-4 | 161 | 0 | - |
| CAT012-3 | 42 | 2 | - |
| COL002-2 | 3 | 0 | - |
| COL002-3 | - | 0 | - |
| COL003-4 | - | 101 | - |
| GEO002-1 | - | - | - |
| GEO006-1 | - | - | - |
| GEO0027-2 | - | - | - |
| GEO0059-2 | - | 152 | 3 |
| GRP048-2 | 1 | 5 | 48 |
| GRP099-1 | 83 | - | - |
| HEN003-1 | 0 | - | - |
| LCL196-1 | 7 | 6 | 23 (A) |
| LCL210-1 | 4 | 7 | 3 (B) |
| NUM003-1 | 0 | 0 | 0 |
| NUM009-1 | 8 | 152 | 0 |
| NUM046-1 | - | - | 2 |
| NUM159-1 | - | - | - |
| NUM232-1 | - | - | 0 |
| NUM284-1 | 0 | - | 0 (C) |
| PLA004-1 | - | - | - |
| PLA011-2 | - | 0 | - |
| PLA014-1 | - | 0 | - |
| PLA014-2 | - | - | - |
| PLA018-1 | - | - | - |
| RNG005-1 | 1 | 199 | 0 |
| RNG038-2 | 0 | 94 | 8 |
| RNG040-1 | 0 | 0 | 0 |
| SET008-1 | 0 | 0 | 0 |
| SET015-2 | - | - | - |
| SET024-6 | 0 | 0 | 0 |
| SET061-6 | 16 | - | 1 |
| SET063-6 | 6 | - | 1 |
| SET075-6 | 42 | - | 2 |
| SET080-6 | 0 | 3 | 0 |
| SET082-6 | 75 | - | 2 |
| SET083-6 | 76 | - | 1 |
| SET101-6 | 0 | 0 | 6 |
| SET196-6 | 69 | 0 | 0 |
| SET232-6 | - | 21 | 1 |
| SET240-6 | - | 30 | 0 |
| SET243-6 | - | - | 6 |
| SET261-6 | - | - | 6 |
| SET558-6 | 0 | - | - |
| SYN200-1 | 0 | 0 | 0 |
| SYN202-1 | 1 | 0 | 0 |
| SYN271-1 | 0 | 0 | 1 |