Abstract FR:

Cette these traite de deduction automatique en logique modale. La premiere partie, intitulee resolution modale, presente des systemes de preuves par resolution pour la logique modale propositionnelle s4, dans la ligne de la methode proposee par l. Farinal dans resolution modal logic (in logique et analyse n#o 110/111). La seconde partie introduit une logique du premier ordre classique, appelee logique des chemins dans laquelle les systemes modaux du premier ordre q, t, q4, s4 et s5 sont traduits. Cette traduction explicite les modalites dans des quantifications du premier ordre et des structures de termes qui s'interpretent comme des chemins dans des modeles de kripke. On met en uvre alors une methode de resolution classique pour la logique des chemins qui fournit, via la traduction une methode de preuves pour les systemes modaux