La notion de théorie s'est séparée de la notion de logique à la fin des années 1920, lorsque Hilbert et Ackermann ont distingué les règles de déduction, indépendantes de l'ob jet du discours, des axiomes qui lui sont spécifiques. S'est alors posée la question de caractériser les théories, définies donc comme des ensembles d'axiomes, que l'on peut utiliser pour formaliser une partie du raisonnement mathématique. Un premier critère est la cohérence de cette théorie : le fait qu'on ne puisse pas démontrer toutes les propositions de cette théorie. Cependant il est progressivement apparu que la cohérence n'était pas une propriété suffisante. Le fait que les démonstrations constructives vérifient les propriétés de la dijonction ou du témoin, ou la complétude de certaines méthodes de démonstration automatique ne découlent pas de la seule cohérence d'une théorie. Mais toutes trois sont par contre conséquentes d'une même propriété : la normalisation des démonstrations. En 1930, le théorème de complétude de Gödel montra que le critére de cohérence pouvait être vu sous différents angles. En plus de la définition précédente interne à la théorie de la démonstration, on peut également définir de manière algébrique la cohérence d'une théorie comme le fait qu'elle possède un modèle. L'équivalence entre ces deux définitions constitue un outil fondamental, qui a permis notamment la démonstration de la cohérence de nombreuses théories : la théorie des ensembles avec la négation de l'axiome du choix par Fraenkel et Mostovski, la théorie des ensembles avec l'axiome du choix et l'hypothèse du continue par Gödel, la théorie des ensembles avec la négation de l'hypothèse du continu par Cohen, . . . A l'inverse, la normalisation des démonstrations semblait ne pouvoir se définir que de manière interne à la théorie de la démonstration. Certains critères inspirés de la théorie des modèles étaient certes parfois utilisés pour démontrer la propriété de normalisation des démonstrations de certaines théories, mais la nécéssité de ces critéres n'avait pas été établie. Nous proposons dans cette thèse un critère algébrique à la fois nécessaire et suffisant pour la normalisation des démonstrations. Nous montrons ainsi que la propriété de normalisation des démonstrations peut également se définir comme un critère algébrique, à l'instar de la propriété de cohérence. Nous avons pour cela défini une nouvelle notion d'algèbre de valeurs de vérités (TVA) appelée algèbres de vérité dépendant du langage (LDTVA). La notion de TVA permet d'exhiber l'algèbre de valeurs de vérité des candidats de réductibilité définis par Girard en 1970. L'existence d'un modèle à valeurs dans cette algèbre définit un critère algébrique suffisant pour la propriété de normalisation des démonstrations. Puis nous avons défini un raffinement de la notion de candidats de réductibilité comme une de ces LDTVAs et avons montré que l'existence d'un modèle à valeurs dans cette algèbre définit un critère algébrique toujours suffisant mais également nécessaire pour la propriété de normalisation des démonstrations. Ce critère est défini pour les cadres logiques de la déduction minimale et du λΠ-calcul modulo. Et nous exhibons finalement la puissance du λΠ-calcul modulo en montrant que tous les systèmes de types purs fonctionnels peuvent être simulés dans ce cadre logique.

La Méthode B est une méthode formelle de spécification et de développement de logiciels critiques largement utilisée dans l'industrie ferroviaire. Elle permet le développement de programmes dit corrects par construction, grâce à une procédure de raffinements successifs d'une spécification abstraite jusqu'à une implantation déterministe du programme. La correction des étapes de raffinement est garantie par la vérification de la correction de formules mathématiques appelées obligations de preuve et exprimées dans la théorie des ensembles de la Méthode B. Les projets industriels utilisant la Méthode B génèrent généralement des milliers d'obligation de preuve. La faisabilité et la rapidité du développement dépendent donc fortement d'outils automatiques pour prouver ces formules mathématiques. Un outil logiciel, appelé Atelier B, spécialement développé pour aider au développement de projet avec la Méthode B, aide les utilisateurs a se décharger des obligations de preuve, automatiquement ou interactivement. Améliorer la vérification automatique des obligations de preuve est donc une tache importante. La solution que nous proposons est d'utiliser Zenon, un outils de déduction automatique pour la logique du premier ordre et qui implémente la méthode des tableaux. La particularité de Zenon est de générer des certificats de preuve, des preuves écrites dans un certain format et qui permettent leur vérification automatique par un outil tiers. La théorie des ensembles de la Méthode B est une théorie des ensembles en logique du premier ordre qui fait appel à des schémas d'axiomes polymorphes. Pour améliorer la preuve automatique avec celle-ci, nous avons étendu l'algorithme de recherche de preuve de Zenon au polymorphisme et à la déduction modulo théorie. Ce nouvel outil, qui constitue le cœur de notre contribution, est appelé Zenon Modulo. L'extension de Zenon au polymorphisme nous a permis de traiter, efficacement et sans encodage, les problèmes utilisant en même temps plusieurs types, par exemple les booléens et les entiers, et des axiomes génériques, tels ceux de la théorie des ensembles de B. La déduction modulo théorie est une extension de la logique du premier ordre à la réécriture des termes et des propositions. Cette méthode est parfaitement adaptée à la recherche de preuve dans les théories axiomatiques puisqu'elle permet de transformer des axiomes en règles de réécriture. Par ce moyen, nous passons d'une recherche de preuve dans des axiomes à du calcul, réduisant ainsi l'explosion combinatoire de la recherche de preuve en présence d'axiomes et compressant la taille des preuves en ne gardant que les étapes intéressantes. La certification des preuves de Zenon Modulo, une autre originalité de nos travaux, est faite à l'aide de Dedukti, un vérificateur universel de preuve qui permet de certifier les preuves provenant de nombreux outils différents, et basé sur la déduction modulo théorie. Ce travail fait parti d'un projet plus large appelé BWare, qui réunit des organismes de recherche académique et des industriels autour de la démonstration automatique d'obligations de preuve dans l'Atelier B. Les partenaires industriels ont fournit à BWare un ensemble d'obligation de preuve venant de vrais projets industriels utilisant la Méthode B, nous permettant ainsi de tester notre outil Zenon Modulo.Les résultats expérimentaux obtenus sur cet ensemble de référence sont particulièrement convaincant puisque Zenon Modulo prouve plus d'obligation de preuve que les outils de déduction automatique de référence au premier ordre. De plus, tous les certificats de preuve produits par Zenon Modulo ont été validés par Dedukti, nous permettant ainsi d'être très confiant dans la correction de notre travail. / The B Method is a formal method heavily used in the railway industry to specify and develop safety-critical software. It allows the development of correct-by-construction programs, thanks to a refinement process from an abstract specification to a deterministic implementation of the program. The soundness of the refinement steps depends on the validity of logical formulas called proof obligations, expressed in a specific typed set theory. Typical industrial projects using the B Method generate thousands of proof obligations, thereby relying on automated tools to discharge as many as possible proof obligations. A specific tool, called Atelier B, designed to implement the B Method and provided with a theorem prover, helps users verify the validity of proof obligations, automatically or interactively. Improving the automated verification of proof obligations is a crucial task for the speed and ease of development. The solution developed in our work is to use Zenon, a first-orderlogic automated theorem prover based on the tableaux method. The particular feature of Zenon is to generate proof certificates, i.e. proof objects that can be verified by external tools. The B Method is based on first-order logic and a specific typed set theory. To improve automated theorem proving in this theory, we extend the proof-search algorithm of Zenon to polymorphism and deduction modulo theory, leading to a new tool called Zenon Modulo which is the main contribution of our work. The extension to polymorphism allows us to deal with problems combining several sorts, like booleans and integers, and generic axioms, like B set theory axioms, without relying on encodings. Deduction modulo theory is an extension of first-order logic with rewriting both on terms and propositions. It is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. This way, we turn proof search among axioms into computations, avoiding unnecessary combinatorial explosion, and reducing the size of proofs by recording only their meaningful steps. To certify Zenon Modulo proofs, we choose to rely on Dedukti, a proof-checker used as a universal backend to verify proofs coming from different theorem provers,and based on deduction modulo theory. This work is part of a larger project called BWare, which gathers academic entities and industrial companies around automated theorem proving for the B Method. These industrial partners provide to BWare a large benchmark of proof obligations coming from real industrial projects using the B Method and allowing us to test our tool Zenon Modulo. The experimental results obtained on this benchmark are particularly conclusive since Zenon Modulo proves more proof obligations than state-of-the-art first-order provers. In addition, all the proof certificates produced by Zenon Modulo on this benchmark are well checked by Dedukti, increasing our confidence in the soundness of our work.