Transfer of Sequent Calculus Strategies to Resolution for S4

This paper illustrates for the propositional S4 a general scheme of transferring strategies of proof search in a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. 1 Introduction This paper presents a general scheme [10, 11] of transforming a cutfree Gentzentype system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov [7] for classical predicate logic. In this way completeness of strategies is first established for the Gentzen-type system, and then transferred to resolution. The method is illustrated here for the propositional S4 in a way very similar to [13]. An adaptation of the Maslov's method to S4 and some of the more elaborate strategies mentioned below are presented in [17]. Let us recapitulate some material from [10, 11, 12]. The main idea of Maslov's met..