The Recursive Resolution method for Modal Logic

In this paper a syntactic proof procedure, Recursive Resolution (RR), will be introduced for a Modal Logic system S4. The RR is analogous to Robinson’s resolution method on predicate calculus. In Predicate Calculus, a well-formed-formula (wff) can be transformed to a set of normal forms (clauses) after a skolemization process where skolem functions are introduced. For any two normal forms, the resolution method tells how to find their resolvent if they are resolvable at all. Similarly, for modal logic S4, there is a preliminary step in RR to transform a wff into a set of normal forms (m-clauses) after a skolemization step of the possibility operator □. For any two normal forms (m-clauses), the RR method determines whether they are modal-resolvable. If so, their modal-resolvent(s) (MR) can be computed. Traditionally, we use the semantic tableau or related method to reason on modal logic which is a direct application of the semantic analysis of the concept of possible world. Computationally, these semantic proof procedures involve unnecessary backtracking and so cannot be efficiently implemented in a computer. RR is also justified by and devised according to the semantic analysis of possible worlds. But it avoids explicit construction of possible worlds or reducing modalities by quantified variables and can be implemented by some recursive functions.