The recursive resolution method for modal logic (Q1104915)

The author suggests a syntactic proof procedure for the modal logic system S4 avoiding explicit construction of possible worlds or reduction of modalities by quantified variables. The basic approach mirrors that of Robinson's resolution for predicate calculus. The originality rises from the introduction of a transformation process for modal clauses which ``Skolemizes'' the possibility operator. It results in obtaining modal clauses in special normal form (m-clause), which can be further processed by the proof procedure called Recursive Resolution (RR). Modal resolution criterion (MRC) is one of the milestones of this procedure. MRC is specified in form of an algorithm (its implementation in Franz LISP is listed in the Appendix), its basic property is stated by the following Theorem 1: A pair of complementary \(m\)-literals is inconsistent iff they satisfy the MRC. Modal resolvability of two \(m\)-clauses is defined through 5 special recursive rules, denoted by SRR, the application of which is proved to be sound. The author conjectures that the SRR rules form a complete decision procedure for a notationally restricted propositional S4.