Zamov, N. K. Modal resolutions. (Russian) Zbl 0689.03005 Izv. Vyssh. Uchebn. Zaved., Mat. 1989, No. 9(328), 22-29 (1989). The resolution method is proposed for the modal propositional logic S4. For using this method for any formula it is necessary to eliminate modal operators by replacing each \(\square\)-operator by a variable and each \(\diamond\)-operator by a constant. As result a monadic predicate formula with functional symbol *, which means concatenation, is obtained. This formula can be reduced to c.n.f. by any known method (distributive transformations, introducing new predicate symbols). Then the traditional resolution method with associative unification is used. Completeness and correctness of this method are shown. The use of some ordering search strategy permits to show that the set of inferable clauses is a finite set for any formula from S4. It follows that this ordering strategy is a decision algorithm for the modal logic S4. The proposed method can be extended to other modal systems: S5, T, K4. Reviewer: N.K.Zamov Cited in 1 ReviewCited in 1 Document MSC: 03B35 Mechanization of proofs and logical operations 03B45 Modal logic (including the logic of norms) 03B25 Decidability of theories and sets of sentences Keywords:resolution method; modal propositional logic S4; associative unification; ordering search strategy; decision algorithm; modal logic PDFBibTeX XMLCite \textit{N. K. Zamov}, Izv. Vyssh. Uchebn. Zaved., Mat. 1989, No. 9(328), 22--29 (1989; Zbl 0689.03005)