×

Modal resolutions. (Russian) Zbl 0689.03005

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

MSC:

03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)
03B25 Decidability of theories and sets of sentences
PDFBibTeX XMLCite