 As in propositional temporal logic, formulae of FOTL are evaluated in first-order temporal models locally at time instants. However, since the formulae of FOTL may contain variables, the notion of truth is relativized not only to a model and a time instant but also to a variable assignment. We denote the set of individual variables of FOTL by \(\mathrm{VAR}\) and the set of individual terms (i.e. variables and constants) by \(\mathrm{TERM}\).