TeMP

TeMP: A temporal monodic prover. First-Order Temporal Logic, FOTL, is an extension of classical first-order logic by temporal operators for a discrete linear model of time (isomorphic to ℕ, that is, the most commonly used model of time). Formulae of this logic are interpreted over structures that associate with each element n of ℕ, representing a moment in time, a first-order structure (D n ,I n ) with its own non-empty domain D n . In this paper we make the expanding domain assumption, that is, D n ⊆D m if n<m. The set of valid formulae of this logic is not recursively enumerable. However, the set of valid monodic formulae is known to be finitely axiomatisable.