Gotowa bibliografia na temat „Démonstration automatisée de théorèmes”

Ce bel ouvrage, clair, aéré et spacieux, se caractérise à la fois par sa volonté de simplicité d'accàs (en particulier pour la première partie, oú l'accent est mis sur le côté opératoire de la logique), et son ambition (deuxiéme partie, plus théorique), puisqu'on y trouve notamment une démonstration de la complétude d'un certain système déductif S1 pour la logique classique des prédicats, ainsi qu'une version synoptique du théorème de Gödel (1931), selon lequel toute thèorie du premier ordre (consistante) complète axiomatisable est décidable, d'où il s'ensuit que l'arithmétique, c'est-à-dire l'ensemble des énoncés du premier ordre vrais dans N, n'est pas axiomatisable; ce qu'on exprime souvent en disant que tout système formel pour l'arithmétique est incomplet, au sens où il y a des énoncés vrais qui ne sont pas des théorèmes du système.

Ce travail se situe dans le cadre de la déduction automatique. Il traite d'une méthode, appelée la schématisation, utilisée pour remédier à des problèmes d'expressivité, d'efficacité et de divergence. La schématisation est un moyen de représentation finie d'ensembles infinis d'objets. Ceux-ci peuvent se retrouver dans différents domaines de l'informatique. Le but de notre travail est l'étude de cette méthode d'un point de vue théorique et pratique. D’un point de vue théorique, nous avons situé les classes de schématisation existantes dans la hiérarchie des langages d'arbres après les avoir comparé entre elles. Chose qui nous a permis de proposer des classes plus expressives que toutes les classes proposées jusqu'ici et qui sont intéressantes pour la déduction automatique. D’un point de vue pratique, nous avons proposé plusieurs algorithmes de manipulation de schématisations. Nous avons surtout introduit la notion de problème d'inclusion pour lequel nous avons donné un algorithme que nous avons applique à la généralisation inductive d'ensembles infinis de termes. Cet algorithme peut trouver d'autres applications dans le génie logiciel, la réécriture et le calcul des processus. Nous avons ensuite améliore l'algorithme classique de généralisation inductive dans ses cas d'échec en utilisant les I-termes puis les B-termes. Les algorithmes proposés peuvent être vus comme des procédures de construction automatique, respectivement, des I-termes et des B-termes.

Implantation de différentes méthodes de démonstration automatique basées sur un algorithme de completion rapide appelé SKB et un algorithme de complétion qui privilégie la règle de simplification par rapport à celle de superposition, nous étudions cet algorithme et son implantation. Étude du filtrage pour la simplification et la réécriture des termes

Il est montre que pour des logiques modales propositionnelles et quantifiees, des formes normales simples peuvent etre obtenues par des methodes de type skolemisation. Par consequent, des procedures automatiques de demonstration comme le principe de resolution, peuvent etre definies. Pour le premier ordre, une correspondance est etablie entre chaque logique modale et une theorie equationnelle particuliere. L'extension de l'algorithme d'unification classique permet alors la mecanisation de la demonstration dans cette logique

Cette thèse part de la volonté d'implanter une bibliothèque de matrices dans l'environnement de développement sûr FoCaLize. Nous donnons une spécification dans laquelle toutes les matrices sur un même anneau commutatif unitaire sont vues comme des éléments d'une algèbre unitaire unique. Dans un tel contexte, les opérateurs d'addition et de multiplication sont des fonctions totales. Cela permet de les coder par des méthodes récursives dans un type de données ne tenant pas compte de la dimension des matrices. Nous recherchons ensuite des spécifications dans la bibliothèque FoCaLize vue comme une base de données de formules du premier ordre. La recherche d'une spécification aboutit s'il existe une formule de la bibliothèque dont l'information cherchée soit une conséquence dans le fragment de la logique du premier ordre des preuves ``quantitatives''. Celles-ci n'utilisent que les règles de quantification du calcul des séquents et se terminent par la règle axiome. Nous établissons un critère nécessaire et suffisant pour la réussite de notre recherche, retrouvant ainsi un résultat connu que nous affinons cependant. Nous donnons deux formalisations équivalentes de notre critère. Nous caractérisons l'admissibilité de la règle de coupure dans notre fragment par une méthode que nous pensons originale. Nous mettons en évidence une condition pour qu'une modification des symboles fonctionnels et relationnels dans un séquent du premier ordre permette d'obtenir un nouveau séquent possédant une preuve quantitative. Nous utilisons ce résultat pour proposer une méthode de réutilisation de preuve par analogie. Nous décrivons comment utiliser ces résultats dans le cadre de FoCaLiZe.

Les logiques sont de puissants outils qui permettent la spécification de systèmes informatiques et la preuve de l'adéquation de leurs implantations avec ces spécifications. Dans le cadre des logiques sous-structurelles, nous mettons en place des outils de démonstration automatique et de construction de contre-modèles. Ces logiques intègrent la notion de ressource ; au niveau de la recherche de preuve, la gestion des ressources permet la mise en place de procédures plus efficaces ; au niveau de l'interprétation sémantique, la notion de ressource permet de construire des modèles fidèles et complets. Nous établissons un lien entre la notion syntaxique de réfutation et la notion sémantique de contre-modèle. Nous en déduisons des méthodes de démonstration de la propriété des modèles finis ainsi que des algorithmes de construction de contre-modèles. En logique intuitionniste propositionnelle, la gestion fine de ressources permet d'en déduire une implantation efficace de la recherche de preuves. En logique intuitionniste linéaire, les modèles à base de ressources permettent une preuve élégante de la propriété des modèles finis. Nous établissons un lien entre la sémantique des ressources et la sémantique à base de réseaux de Petri, ce qui permet de raffiner les résultats de complétude partiels connus jusqu'alors
Logics can be used as powerful tools for specifying computer systems and proving the soundness of their implementations with respect to these specifications. In the field of substructural logics, we develop tools and methods for automated deduction and counter-model generation. These logics involve the notion of resource : at the level of proof-search, the management of resources enables more efficient procedures : at the semantic level, resource models provide sound and complete interpretations. We develop a link between the syntactic notion of refutation and the semantic notion of counter-model. We deduce methods for proving the finite model property and algorithms for implementation of a proof-search procedure, based on a fine management of resources. In intuitionistic linear logic, resource based models constitute the core of an elegant proof of the finite model property. Furthermore, we establish a link between resource models and Petri net based models, from which we improve the proeceding partial completness results

En depit des nombreuses strategies ameliorant l'algorithme de sl resolution, beaucoup d'informations redondantes et inutiles etaient generees, notamment lors d'echec d'effacement de litteraux. Un algorithme, appele slri, est propose. Il tient compte de ces informations. Il est demontre que l'arbre de recherche de cet algorithme est inclus dans l'arbre de recherche de la sl resolution

Nous nous intéressons dans cette thèse à la preuve formelle de correction des analyses statiques. Nous nous basons sur la théorie de l'interprétation abstraite qui présente une analyse statique comme une sémantique approchée d'un programme. Nous utilisons l'assistant de preuve Coq qui permet d'extraire le contenu calculatoire d'une preuve constructive. L'implémentation Caml certifiée d'une analyse peut ainsi être extraite de la preuve d'existence, pour tout programme, d'une approximation correcte de la sémantique concrète de ce programme. Nous présentons un cadre théorique fondé sur l'interprétation abstraite et permettant le développement formel d'une large gamme d'analyses statiques. Une bibliothèque Coq de construction modulaire de treillis est ensuite proposée. Des preuves complexes de terminaison de calcul itératif de point fixe peuvent ainsi Ítre construites par simple composition de foncteurs. Plusieurs cas d'études pour l'analyse de programme en bytecode Java sont présentés.

Cette étude présente un nouveau développement de techniques formelles de spécification et de preuve en modélisation géométrique. Le modèle topologique des cartes combinatoires est axiomatisé dans le calcul des constructions inductives (CCI), une théorie des types bien adaptée à la mécanisation des mathématiques en logique d'ordre supérieur. Une hiérarchie de types abstraits spécifiant les cartes combinatoires est construite et validée par des preuves inductives de consistance et de complétude dans le système Coq, un assistant à la preuve implantant le CCI. Un prototype certifié est obtenu par l'extraction automatique d'algorithmes fonctionnels des preuves constructives de leur correction. Des difficultés classiques en spécification formelle et preuve de théorèmes - comme la cohabitation d'objets et de leur généralisation dans la même hiérarchie, la gestion élégante du sous-typage, la complétion de relations et d'objets partiels, la confrontation des approches constructive et observationnelle, et la symétrisation de relations - sont abordées, non seulement sur le plan des spécifications formelles et de la preuve, mais aussi du point de vue de l'extraction. Grâce notamment à la nouvelle notion de quasi-face, des questions délicates de modélisation géométrique - comme la notion de face, l'énoncé d'un critère de planarité, la preuve de la formule d'Euler et d'un théorème de Jordan topologique - sont ainsi résolues d'une façon originale et incontestable, offrant une grande pénétration des fondements topologiques de la modélisation géométrique et une profonde compréhension du modèle. Une méthodologie de spécification et de preuve applicable à d'autres domaines est enfin proposée.

Le concept central de théorème désigne une assertion justifiée par un argument irréfutable agencé selon des règles formelles, qu'on appelle une preuve. Prouver des théorèmes est utile à la fois en Informatique et en Mathématiques. Cependant, beaucoup de théorèmes utiles, tels que ceux engendrés par la vérification formelle qu'un programme respecte une spécification, sont trop pénibles et inintéressants pour mériter l'attention d'experts humains; plusieurs décennies de recherches ont donc été consacrées au domaine de la démonstration automatique. La Superposition est une technique efficace permettant de prouver les théorèmes exprimés en logique du premier ordre avec égalité (en bref, la capacité de remplacer mutuellement deux objets égaux dans n'importe quelle expression). Pourtant, la Superposition montre ses limites dans beaucoup de cas où des théories spécifiques ou du raisonnement par récurrence sont nécessaires. Dans cette thèse, nous développons de nouvelles extensions à la Superposition; nous soutenons que cette dernière se prête bien à l'ajout de règles d'inférence et de mécanismes de raisonnement supplémentaires. Tout d'abord, nous développons un système d'inférence qui donne à la Superposition les moyens de raisonner dans l'arithmétique linéaire entière, une théorie activement utilisée et étudiée dans d'autres domaines de la preuve automatique tels que SMT (Satisfiabilité Modulo Théories). L'arithmétique peut également permettre des encodages vers la logique du premier ordre plus efficaces pour les structures discrètes totalement ordonnées, par exemple, la logique temporelle. Nous définissons ensuite un mécanisme permettant aux prouveurs fondés sur la Superposition de raisonner par récurrence sur des types algébriques (naturels, listes, arbres binaires, etc. ) Le raisonnement par récurrence est très courant en Mathématiques et en Informatique, mais son intégration dans les systèmes de preuve dédiés à la logique du premier ordre a été peu étudiée. Enfin, nous présentons un système de détections de théories axiomatiques capable de déceler la présence de structures algébriques connues dans un ensemble de formules. Ce système rappelle la manière dont un mathématicien qui étudie un nouvel objet peut découvrir que ce dernier relève d'une structure connue comme les groupes — ce qui lui permet de mobiliser ses connaissances sur cette théorie. Cette thèse comprend également une part importante de travail d'implémentation : toutes les contributions listées ci-dessus ont été incorporées dans une bibliothèque et un prouveur automatique, Zipperposition; tous deux sont écrits en OCaml et publiés sous licence libre
The central concept of theorem designates a claim backed by an irrefutable argument that follows formal rules, called a proof. Proving theorems is very useful in both Computer Science and Mathematics. However, many theorems are too boring and tedious for human experts (for instance, theorems generated to ensure that software abides by some specification); hence the decades-long effort in automated theorem proving, the field dedicated to writing programs that find proofs. Superposition is a very competitive technique for proving theorems in the language of first-order logic with equality over uninterpreted functions (in a nutshell, being able to replace equals by equals in any expression). Even then, Superposition falls short for many problems that require theory-specific reasoning or inductive proofs. In this thesis, we aim at developing new extensions to Superposition. Our claim is that Superposition lends itself very well to being grafted additional inference rules and reasoning mechanisms. First, we develop a Superposition-based calculus for integer linear arithmetic. Linear Integer Arithmetic is a widely studied and used theory in other areas of automated deduction, in particular SMT (Satisfiability Modulo Theory). This theory might also prove useful for problems that have a discrete, totally ordered structure, such as temporal logic, and that might be encoded efficiently into first-order logic with arithmetic. Then, we define an extension of Superposition that is able to reason by structural induction (natural numbers, lists, binary trees, etc. ) Inductive reasoning is pervasive in Mathematics and Computer Science but its integration into general purpose first-order provers has not been studied much. Last, we present a theory detection system that, given a signature-agnostic description of algebraic theories, detects their presence in sets of formulas. This system is akin to the way a mathematician who studies a new object discovers that this object belong to some known structure, such as groups, allowing her to leverage the large body of knowledge on this specific theory. A large implementation effort was also carried out in this thesis; all the contributions presented above have been implemented in a library and a theorem prover, Zipperposition, both written in OCaml and released under a free software license

Nous étudions des méthodes de recherche simultanée de refutation et de modèle. Nous proposons une méthode pour la construction de modèles finis réduisant de façon importante l'espace de recherche des approches existantes. Nous nous intéressons ensuite à la recherche de modèles infinis. Nous étendons les méthodes RAMC (Refutation And Model Construction) et RAMCET (Refutation And Model Construction with Equational Tableaux) définie par R. Caferra et N. Zabel en introduisant de nouvelles règles et stratégies. Ces extensions augmentent strictement les capacités de la méthode, à la fois pour la recherche de preuve et de contre-exemple. Nous montrons que les méthodes proposées sont des procédures de décision uniforme pour une large clase de formules logiques. Ensuite, nous proposons et étudions de nouveaux formalismes pour représenter les modèles: les termes avec exposants entiers et les automates d'arbres. Nous prouvons la décidabilité de la théorie du premier ordre sur les termes avec exposants. Nous proposons également une nouvelle approche pour la découverte et l'utilisation de l'analogie en recherche simultanée de preuve et de contre-exemple et nous montrons comment utiliser la méthode RAMC en Programmation Logique (pour étendre les capacités des interpréteurs, détecter, voire corriger des erreurs dans les programmes etc. ). Enfin, nous décrivons le système RAMC-ATINF implémentant certaines des idées proposées et nous donnons quelques résultats expérimentaux
In this thesis, we present several new techniques for model building in Automated Deduction. In the first part, we propose a general method for building finite models that favourably compares with the most powerful existing finite model builders. In the second part, we investigate methods for simultaneous search for refutations and (infinite, Herbrand) models. We improve the methods RAMC (Refutation And Model Construction) and RAMCET (Refutation And Model Construction with Equational Tableaux) defined by R. Caferra and N. Zabel by defining new rules and strategies. These extensions strictly increase the capabilities of the methods both for model building and unsatisfiability detection. We show that some of the proposed methods are uniform decision procedures for a wide range of decidable classes. We show the limits of the formalism of equational constraints, previously used for representing Herbrand models, and we propose to extend it by including terms with integer exponents (I-terms) and tree automata. As a new result, we prove the decidability of the first-order theory of I-terms. Fourthly, we study some applications of our work: we present a new approach for discovering and using analogy in simultaneous search for refutations and models, and we show how to use the method RAMC in Logic Programming (for extending logic program interpreters, detecting and correcting errors in logic programs etc. ). Finally we describe the system RAMC-ATINF implementing our approach and we report some experiments showing the practical capabilities of our method