Modal Theorem Proving: An Equational Viewpoint

Abstract

We propose a new method for automated theorem proving in first order modal logic. Essentially, the method consists in a translation of modal logic into a specially designed typed first order logic cal led Path Logic, such that classical modal systems (first order Q, T, 04, S4, SS) can be characterized by sets of equations. The question of modal theorem proving then amounts to classical theorem proving in some equational theories. Different methods can be . investigated and in this paper we consider Resolution. We may use Resolution with Paramodulation, or a combination of Resolution and Rewriting techniques. In both cases, known results provide "free of charge" a framework immediately applicable to Path Logic, with completeness theorems. Considering efficiency, the R~writing method seems better and we present here in details its application to Path Logic. In particular we show how it is possible to define a special kind of skolemisation and design a unification algorithm which insures that two clauses will always have a finite set of resolvents.