L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé de calcul dans ces systèmes consiste en « l'élimination des coupures ». Deux interprétations sont considérées.<br /><br />Le lambda-calcul constitue le support de la première interprétation. Nous établissons une correspondance de type Curry-Howard entre LJ et une variante syntaxique du lambda-calcul avec opérateur explicite de substitution (de type « let _ in _ »). Une procédure de normalisation/élimination des coupures confluente et terminant fortement est donnée et l'extension de la correspondance à LK se fait en considérant l'opérateur mu du lambda-mu-calcul de Parigot.<br /><br />La théorie des jeux constitue le support de la deuxième interprétation: les preuves des calculs des séquents sont vues comme des stratégies gagnantes pour certains types de jeux à deux joueurs (dialogues) se disputant la validité de la formule prouvée. Nous donnons deux résultats.<br /><br />Dans un premier temps, nous montrons qu'il suffit de considérer des restrictions LJQ de LJ puis LKQ de LK pour établir, dans le cas propositionnel, une bijection entre les preuves de ces systèmes et les E-dialogues intuitionnistes puis classiques définis par Lorenzen dans un but de fondement de la prouvabilité en termes de jeux. Ceci affine et généralise un résultat de Felscher d'équivalence entre l'existence d'une preuve d'une formule A dans LJ et l'existence d'une stratégie gagnante pour le premier des joueurs dans un E-dialogue à propos de A.<br /><br />Dans un deuxième temps, nous partons d'une logique propositionnelle infinitaire sans variable considérée par Coquand pour y définir une interaction prouvée terminante entre les preuves vues comme stratégies gagnantes. Nous montrons une correspondance opérationnelle entre ce procédé d'interaction et l'élimination « faible de tête » des coupures, celle-ci étant indépendamment prouvée terminante.

Le langage est conçu de manière à permettre une interprétation synchrone des suites. La nature du langage (dont la sémantique s'exprime simplement) permet des manipulations formelles sur les programmes dans le but de faire des vérifications et des preuves de correction. Des exemples illustrent l'utilisation du langage pour la programmation de systèmes temporisés pris dans différents domaines (temps réel classique, automatique, systolique, spécification et conception des circuits)

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