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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element