Abstract FR:

Le but de ce travail consiste a etendre au calcul des predicats la methode de resolution pour la logique propositionnelle modale qui a ete definie par m. Luis farinas del cerro. Le systeme modal considere, appele q, est un sous-systeme de ceux plus connus, t, s4 et s5. Nous considerons toutefois que les resultats obtenus dans ce travail peuvent facilement etre etendus a ceux-ci. Nous definissons une propriete de herbrand modale pour le systeme q et en donnons la preuve. Cette propriete nous permet ensuite de definir un systeme de regles de resolution dans lequel l'unification des termes est soumise a certaines restrictions, et d'en prouver sa correction et sa completude