 First-order temporal logics are very expressive, and this often comes with a high computational price: these logics can be deductively very complex and are typically highly undecidable (cf. Merz 1992; Gabbay et al. 1994; Hodkinson et al. 2002). The first-order temporal logic with constant domain semantics over the natural numbers, for example, with only two variables and unary relation symbols, is not only undecidable but not even recursively axiomatizable (cf. Börger et al. 1997; Hodkinson et al. 2000).