Guarded fragments with constants
Balder ten Cate, Massimo Franceschet

Abstract:
We prove EXPTIME-completeness of the satisfiability problem for
guarded and loosely guarded first-order formulas with a bounded number
of variables and an unbounded number of constants. Guarded fragments
with constants are interesting because of their connection to hybrid
logic.