Decidable fragments of first-order modal logics

Abstract

Abstract The paper considers the set of first-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 satisfiability criterion for formulas in , which reduces the modal satisfiability 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.