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

La thèse est que la représentation par contraintes, en terme de langage et la déduction par la gestion automatique des réseaux de contraintes est une voie adéquate pour les systèmes d'aide à la conception en ingénierie. Deux techniques de l'Intelligence Artificielle à savoir la Propagation de Contraintes et le Raisonnement Qualitatif sont abordées. La Propagation de Contraintes est un mécanisme d'inférences déductives sur les réseaux de contraintes. Ce mécanisme présente plusieurs difficultés, particulièrement dans les calculs pas-à-pas de la résolution des relations entre valeurs des variables. Pour améliorer ce mécanisme, il est proposé dans le présente travail des algorithmes de filtrage sur la consistance locale dans des réseaux de contraintes algébriques n-aires. Ainsi, le concept de réseaux dynamiques est exploité comme un module d'aide à la conception. Le Raisonnement Qualitatif permet aux concepteurs d'analyser les modèles quand la connaissance est incomplète. L'approche de la Simulation Qualitative est proposée. L'adéquation de celle-ci est illustrée par d'une part, la représentation de connaissances incomplètes en termes de contraintes qualitatives, et d'autre part, sa capacité de saisir les comportements qualitatifs possibles des modèles. Un ensemble de logiciels est développé et leur efficacité démontrée sur des cas simples.