Deciding the guarded fragments by resolution

The guarded fragment (GF) is a fragment of first-order logic that has been introduced for two main reasons: first, to explain the good computational and logical behaviour of propositional modal logics. Second, to serve as a breeding ground for well-behaved process logics. In this paper we give resolution-based decision procedures for the GF and for the loosely guarded fragment (LGF) (sometimes also called the pairwise guarded fragment). By constructing an implementable decision procedure for the GF and for the LGF, we obtain an effective procedure for deciding modal logics that can be embedded into these fragments. The procedures have been implemented in the theorem prover Bliksem.