Abstract FR:

L'objectif de ce travail est d'apporter une contribution à l'évolution des techniques développées en démonstration automatique et en programmation logique, par l'étude et la mise en oeuvre d'un système de programmation logique : le système STRALOG. Cette thèse propose dans une première partie une présentation des concepts théoriques à la base des systèmes de démonstration automatique : systèmes formels, syntaxe et sémantique de la logique des prédicats du 1er ordre, principe de résolution et une étude détaillée des stratégies de résolution qui ont été développées (correction et complétude des méthodes). Nous avons consacré la deuxième partie de ce travail à un état de l'art des systèmes existants : le langage Prolog, les systèmes "Prolog Technology Theorem Prover" de M. E. Stickel, "Near-Horn Prolog" de D. W. Loveland et le système de D. A. Plaisted. La dernière partie de ce travail est consacrée au système STRALOG que nous avons developpé. Nous présentons les méthodes de résolution mises en oeuvre dans le système. STRALOG utilise des stratégies de résolution basées sur la résolution sémantique et propose des techniques d'optimisation telles que la subsumption, la simplification et la notion d'ordre. Des critères d'efficacité en terme d'espace de recherche et de temps sont considérés. La correction et la complétude de ces méthodes sont étudiées. Nous proposons une comparaison des mécanismes dans STRALOG avec les méthodes appliquées dans les systèmes décrits dans la deuxième partie de cette thèse. STRALOG propose, dans un souci de souplesse d'utilisation du système pour le programmeur et dans une optique programmation logique, un certain nombre de prédicats prédéfinis et notamment un prédicat not qui permet de modéliser un mode de raisonnement révisable. Différents exemples sont décrits ainsi que l'implantation du système. STRALOG a été développé sur station SUN 3/160 en langage C.