|
Abstract : |
Abstract. The paper considers the set ML1 of rst-order polymodal formulas the modal operators in which can be applied to subformulas of at most one free variable. Using a mosaic technique, we prove a general satisability criterion for formulas in ML1, which reduces the modal satisability to the classical one. The criterion is then used to single out a number of new, in a sense optimal, decidable fragments of various modal predicate logics. x1. Introduction. The classical decision problem|to single out expressive and decidable fragments of rst-order logic|has a long history and hardly needs any justication: after all, classical rst-order logic was and still remains in the very center of logical studies, both in mathematics and applications. Here are only three examples (out of dozens) of such fragments (the choice is not, |
