Après un historique bref et général de la déduction automatique, on analyse les tendances actuelles et les besoins en présentation de preuves et communication d'outils d'inférence. Les notions théoriques concernées sont présentées et étudiées en détail. On donne ensuite une synthèse comparative critique et exhaustive de l'état de l'art. Cette synthèse manquait dans la littérature. L'analyse des notions fondamentales en logique et la synthèse sur l'état de l'art permettent d'établir les caractéristiques retenues pour le système GLEF (Graphical & Logical Edition Framework). La conception et la réalisation de deux langages ont permis de rendre GLEF générique (c'est à dire paramétrable par le système formel employé et par la présentation de ses preuves). Un formalisme de définition, fondé sur le Calcul des Construction (dû à Coquand et Huet), sert à représenter et à vérifier les systèmes formels et les preuves dans ses systèmes formels. Un langage de présentation, fondé sur la notion de «boîte», sert à décrire leur présentation. En annexe nous donnons un algorithme original pour l'opération d'effacement, particulièrement difficile en lambda-calcul typé, qui sert à réaliser la commande «couper» de GLEF. GLEF a été développé au sein du projet ATINF (ATelier d'INFérence). Un manuel utilisateur rudimentaire et de nombreux exemples d'utilisation en sont donnés. Certains exemples montrent comment, après avoir spécifié la définition et la présentation d'un système formel objet, un utilisateur de GLEF peut construire ou visualiser des preuves en manipulant directement les objets (formules, preuves partielles, etc.) à l'écran, avec la souris. D'autres illustrent comment GLEF présente les preuves produites par les démonstrateurs d'ATINF ou extérieurs à ATINF. Les principales lignes de recherche future concluent ce travail

Une technique d'abstraction et de partage de structure pour une methode de démonstration automatique non expérimentée jusqu'à présent est proposée. On donne aussi une généralisation de la règle d'inférence pour le cas propositionnel. Une preuve est séparée en plan + validation, ce qui correspond à séparer la partie purement déductive de l'algorithme d'unification. Cette séparation est utilisée pour détecter les ensembles responsables des échecs de validation pour un retour arrière non aveugle

Etude des résolutions de problèmes mathématiques par des personnes parvenues au stade hypothético-déductif exprimées par un discours. Présentation d'un outil pour l'étude des raisonnements naturels.

Les motivations initiales de ce travail proviennent de l'étalonnage de caméras en vision artificielle. Nous nous sommes surtout intéressés aux manières d'exploiter des mesures dans les images (détection d'objets) et des considérations géométriques formelles. Nous avons élargi nos recherches à la problématique suivante :"l'interaction entre symbolique et numérique ". Ce travail se divise en trois parties. La première partie traite de la résolution d'équations polynomiales avec des coefficients approchés. Nous étudions des méthodes matricielles qui transforment la résolution en la recherche des valeurs et des vecteurs propres d'une matrice. Ces transformations et et les calculs de valeurs et vecteurs propres sont continues par rapport aux coefficients et permettent donc de résoudre des équations à coefficients approchés. La deuxième partie présente un cadre algébrique permettant d'exprimer simplement des contraintes géométriques. Ce formalisme nous a permis de modéliser de manière fine l'étalonnage d'une ou plusieurs caméras avec l'aide d'un plan. L'étalonnage ne peut être effectué pratiquement qu'avec des résolutions numériques de systèmes linéaires. La troisième partie est consacrée à l'étude et surtout à l'utilisation des outils de démonstration automatique en géométrie pour la construction de modèles 3D articulés. Par des optimisations numériques, nous déterminons les paramètres des modèles articulés qui permettent aux images de ces modèles de coïncider avec les données extraites des photographies

Cette thèse d'habilitation contient un traitement systématique des algorithmes d'élimination pour décomposer des systèmes arbitraires de polynômes à plusieurs variables en systèmes triangulaires de différentes sortes (réguliers, simples, irréductibles, ou munis de propriétés de projection), en fournissant les décompositions des ensembles des zéros associés. Beaucoup de ces algorithmes et les théories sous-jacentes sont proposés et développés par l'auteur sur la base des travaux de J.F. Ritt, W.-t. Wu, A. Seidenberg et J.M. Thomas. Certains algorithmes pertinents comme ceux fondés sur les résultants ou les bases de Groebner sont passés en revue. Des applications de ces méthodes d'élimination sont présentées, concernant des aspects algorithmiques en géométrie algébrique, la théorie des idéaux de polynômes, la résolution des systèmes algébriques, la démonstration automatique en géométrie, etc.

La confiance formelle en une propriété abstraite provient de l'existence d'une preuve de sa correction, qu'il s'agisse d'un théorème mathématique ou d'une qualité du comportement d'un logiciel ou processeur. Il existe de nombreuses définitions différentes de ce qu'est une preuve, selon par exemple qu'elle est écrite soit par des humains soit par des machines, mais ces définitions sont toutes concernées par le problème d'établir qu'un document représente en fait une preuve correcte. Le cadre des Certificats de Preuve Fondamentaux (Foundational Proof Certificates, FPC) est une approche proposée récemment pour étudier ce problème, fondée sur des progrès de la théorie de la démonstration pour définir la sémantique des formats de preuve. Les preuves ainsi définies peuvent être vérifiées indépendamment par un noyau vérificateur de confiance codé dans un langage de programmation logique. Cette thèse étend des résultats initiaux sur la certification de preuves du premier ordre en explorant plusieurs dimensions logiques essentielles, organisées en combinaisons correspondant à leur usage en pratique: d'abord, la logique classique sans points fixes, dont les preuves sont générées par des démonstrateurs automatiques de théorème; ensuite, la logique intuitionniste avec points fixes et égalité,dont les preuves sont générées par des assistants de preuve. Les certificats de preuve ne se limitent pas comme précédemment à servir de représentation des preuves complètes pour les vérifier indépendamment. Leur rôle s'étend pour englober des transformations de preuve qui peuvent enrichir ou compacter leur représentation. Ces transformations peuvent rendre des certificats plus simples opérationnellement, ce qui motive la construction d'une suite de vérificateurs de preuve de plus en plus fiables et performants. Une autre nouvelle fonction des certificats de preuve est l'écriture d'aperçus de preuve de haut niveau, qui expriment des schémas de preuve tels qu'ils sont employés dans la pratique des mathématiciens, ou dans des techniques automatiques comme le property-based testing. Ces développements s'appliquent à la certification intégrale de résultats générés par deux familles majeures de démonstrateurs automatiques de théorème, utilisant techniques de résolution et satisfaisabilité, ainsi qu'à la création de langages programmables de description de preuve pour un assistant de preuve. / Formal trust in an abstract property, be it a mathematical result or a quality of the behavior of a computer program or a piece of hardware, is founded on the existence of a proof of its correctness. Many different kinds of proofs are written by mathematicians or generated by theorem provers, with the common problem of ascertaining whether those claimed proofs are themselves correct. The recently proposed Foundational Proof Certificate (FPC) framework harnesses advances in proof theory to define the semantics of proof formats, which can be verified by an independent and trusted proof checking kernel written in a logic programming language. This thesis extends initial results in certification of first-order proofs in several directions. It covers various essential logical axes grouped in meaningful combinations as they occur in practice: first,classical logic without fixed points and proofs generated by automated theorem provers; later, intuitionistic logic with fixed points and equality as logical connectives and proofs generated by proof assistants. The role of proof certificates is no longer limited to representing complete proofs to enable independent checking, but is extended to model proof transformations where details can be added to or subtracted from a certificate. These transformations yield operationally simpler certificates, around which increasingly trustworthy and performant proof checkers are constructed. Another new role of proof certificates is writing high-level proof outlines, which can be used to represent standard proof patterns as written by mathematicians, as well as automated techniques like property-based testing. We apply these developments to fully certify results produced by two families of standard automated theorem provers: resolution- and satisfiability-based. Another application is the design of programmable proof description languages for a proof assistant.