Abstract FR:

Nous étudions dans ce travail des méthodes de déduction automatique pour la logique multi-modale. Dans une première partie les logiques multi-modales considérées contiennent un nombre fini de paires d'opérateurs modaux. Dans la dernière partie les opérateurs modaux peuvent être indexés par des termes d'une logique à sortes ordonnées. Dans les deux cas les opérateurs modaux sont de type KD, KD4, KT, KT4 ou KF. Les formules de la logique multi-modale sont traduites dans une logique du premier ordre à sortes ordonnées. Dans le premier cas la logique utilisée est munie d'une théorie équationnelle. Dans le deuxième cas, nous utilisons en plus une théorie de contraintes. Pour la déduction automatique les méthodes utilisées sont adaptées de la E-résolution de Plotkin et de la résolution contrainte de Frisch. Les théories équationnelles utilisées possèdent un opérateur associatif mais les termes obtenus par traduction possèdent une structure très particulière (appelée ici propriété PR) et un procédé adapté de skolémisation permet de conserver cette structure. Une étude de l'unification associative pour les termes possédant cette propriété est faite pour l'algorithme de Plotkin et pour des algorithmes utilisant des règles de transition. Les algorithmes proposés terminent et calculent des ensembles complets d'unificateurs, qui sont, dans ce cas, finis.