Linear strategy for propositional modal resolution (Q1113888)

A resolution method for propositional modal logic developed by \textit{L. Fariñas del Cerro} [Logique Anal., Nouv. Sér. 28, 153-172 (1985; Zbl 0631.03007)] is refined to linear modal resolution; the modal system on which the calculus is based is S4. The difference between classical and modal clause logic is that the latter does not admit a complete elimination of the hierarchical formula structure. The key notion is that of S-deduction; it is defined as a sequence of formulas \(S_ 0,...,S_ n\) s.t. \(S_{i+1}\) is defined by \(S_ i\) in one step (there are four rules for a step). A linear S-deduction is defined by marking some subformulas as lemmas and using the lastly defined lemmas for the next inference step. The main part of the paper consists of the proof of completeness, which is in the spirit of tableau methods for modal logic. It could be worth to alter the terminology and some techniques applied in the paper in order to improve the clarity.