Abstract FR:

Le but de cette these est de presenter une etude ainsi que la realisation d'un atelier de demonstration automatique multilogiques, a savoir logique du 1er ordre, logique avec sortes ordonnees, logique modale. L'architecture de l'atelier est presentee ainsi que les concepts qu'il met en uvre, abstraction, modularite, reutilisabilite et efficacite. Dans la seconde partie, nous presentons une application particuliere a la logique modale en transformant les formules dans un type de logique equationnelle avec sortes, la logique des chemins. Nous presentons differents algorithmes d'unification particuliers ainsi que la methode de comparaison associee. Nous obtenons par cette methode des gains importants en nombre d'unificateurs, diminuant ainsi l'espace de recherche