Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

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

" Eyu ", l'Homme, naît riche, c'est la société qui l'appauvrit par le biais des institutions qui établissent les catégories de pensée et les règles sur lesquelles les individus s'appuient pour penser et agir. À Bokokopé au Togo, des migrants de l'ethnie dite kabyè bénéficient de projets de développement, notamment en agriculture et en élevage. Le but de ces projets est d'augmenter le revenu de ces paysans, garanti d'une amélioration de conditions de vie et de bien-être. Mais les différents acteurs de ce processus ne partagent pas ce style de pensée qui lie le bien-être au revenu. Ce qui entraine, des difficultés à s'entendre sur les indicateurs à adopter lors des différentes évaluations. L'outil principal des techniciens du développement est le cadre logique. Il s'agit d'un tableau à double entrées qui enregistre, d'un côté la logique interne de l'activité à mener, et de l'autre les critères de mesure. Toute action non-logique et non mesurable est par conséquent presque exclue. C'est ainsi que, lorsque Hazou décide par exemple de revendre sa chèvre "à perte" en justifiant qu'il "gagnait en amitié", cela suscite interrogation. Pourquoi résiste-t-il au calcul de rentabilité, moyen incontournable pour améliorer son revenu ? Cette réticence à tout calculer, tout quantifier et tout marchandiser peut se comprendre en se référant à la perception du monde qu'ont les acteurs en présence à Bokokopé ainsi que des rapports qu'ils entretiennent avec le travail et l'argent dans une perspective du vivre ensemble. Leurs actions sont déterminées par plusieurs mondes de pensée qui fluctuent entre des principes marchands portés essentiellement par certaines organisations de développement, et des principes non-marchands véhiculés principalement par des mythes ou des rites auxquels adhèrent les membres de la communauté. Pour les techniciens du développement qui accompagnent ces paysans, la richesse se mesure en argent et en quantité de biens et services produits ou acquis. Les biens difficilement quantifiables et les services gratuits en sont exclus. Dans le monde de pensée dominant à Bokokopé, la richesse, " ñɩm ", ne saurait se limiter à la seule dimension quantitative et mesurable en argent et en biens accumulés qui n'est qu'une manifestation de la représentation de l'Univers Réel (matériel) à côté duquel se mêlent l'Humanité réelle (psychique), l'Univers Sur-réel (religieux) et l'Humanité Sur-réelle (spirituel). La richesse, " ñɩm ", serait donc une eurythmie de ces quatre dimensions qui pré-existe à " Eyu ", l'Homme.