Démonstration automatique en théorie des types

Les logiciels d'aide à la démonstration se répartissent entre prouveurs automatiques et assistants de preuve interactifs. Les premiers sont des outils spécialisés dont les techniques sont éloignées des méthodes intuitives de raisonnement mais dont la portée est faible. Les seconds ont un champ d'application plus large mais l'utilisateur doit expliciter tous les détails de la démonstration. L'automatisation des preuves y est difficile car la logique utilisée est plus expressive. La thèse se compose de trois contributions dans ce domaine. D'abord, nous présentons une extension de la clôture de congruence à une théorie des constructeurs avec application partielle. Un algorithme pour résoudre ce problème est décrit et étudié. Ensuite nous construisons un formalisme du premier ordre incluant des connecteurs définis comme des types inductifs non récursifs dans l'esprit du Calcul des Constructions Inductives. Nous présentons un nouveau calcul de séquents sans contraction pour la logique intuitionniste du premier ordre, adapté à ce formalisme, et prouvons ses propriétés fondamentales: élimination des contractions et des coupures. Nous en dérivons une procédure de semi-décision. Ces deux premières contributions sont implantées dans l'assistant de preuve Coq; la troisième est la description d'une méthode d'interprétation des preuves au premier ordre dans la Théorie des Types grâce à la réflexion calculatoire. Ce paradigme est appliqué à la logique propositionnelle et utilisé par une procédure de décision du système Coq. Cette méthode est aussi étendue au premier ordre avec égalité et permet de vérifier des preuves engendrées par complétion ordonnée dans le système CiME.Among software designed to help formal reasoning, there are automated theorem provers and interactive proof assistants. The former are specialized tools using technics that differ from traditionnal reasoning methods, but they have a very limited range. The latter have a wider range but theii users must specify explicitly every proof step. Automation of proofs is tricky in these latter tools because they use expressive logical systems. This thesis is build around three contributions in this field. First, we present an extension of congruence-closure the a theory of constructors with partial application. An algorithm to solve this problem is described and studied. Then, we build a first-order formalism including connectives defined as non-recursive inductive types similar to those in the Calculus of Inductive Constructions. We present a new contraction-free sequent calculus for first-order intuitionistic logic that is adapted to this formalism, and we prove its fundamental properties: contraction- and cut-elimination. We derive a semi-decision procedure from these results. Those two contributions are implemented inside the Coq proof assistant; the third one is the description of a methode allowing the interpretation of first-order proof tree into Type Theory by computational reflection. This paradigm is applied to propositionnal logic and is used by a decision procedure inside the Coq system. This method is also adapted to first-order logic with equality and allows to check proofs obtained by ordered completion in the CiME system.ORSAY-PARIS 11-BU Sciences (914712101) / SudocSudocFranceF