Abstract FR:

Ce memoire presente une methode de construction d'interfaces pour un ensemble de systemes que l'on groupe sous le terme de moteurs logiques. La particularite de cette methode est l'utilisation d'un modele distribue. Apres la presentation du modele et de sa boite a outils de construction, il est presente deux applications. La premiere application s'interesse a la construction d'un outil de mise au point interactif. En utilisant notre modele, l'environnement de mise au point est obtenu par espionnage de l'evaluateur. Cette technique d'espionnage assure une independance entre l'evaluateur et son outil de mise au point. A l'aide du langage reactif esterel, il est developpe un eventail de comportements qui illustre la flexibilite de l'approche proposee. La deuxieme application concerne la construction d'environnements de preuve. Deux cas d'etude sont presentes. Le premier cas s'interesse a un demonstrateur en logique intuitionniste du premier ordre. La simplicite de cet exemple permet la mise en uvre d'un environnement de preuve ou les preuves sont presentees en langage naturel et construites par des selections a la souris. Le deuxieme cas d'etude presente la construction d'un environnement de preuve pour un demonstrateur grandeur reelle. Cette construction permet de s'interesser plus particulierement a certains aspects comme les performances des interfaces obtenues ou la gestion de l'ensemble des theoremes deja prouves