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
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Song, Fu; Wu, Zhilin: On temporal logics with data variable quantifications: decidability and complexity (2016)
- Fisher, Michael: An introduction to practical formal methods using temporal logic (2011)
- Ludwig, Michel; Hustadt, Ullrich: Fair derivations in monodic temporal reasoning (2009)
- Dixon, Clare: Using temporal logics of knowledge for specification and verification -- a case study (2006)
- Fisher, Michael: Implementing temporal logics: tools for execution and proof (2006)
- Horrocks, Ian; Voronkov, Andrei: Reasoning support for expressive ontology languages using a theorem prover (2006)
- Fernández-Gago, M.C.; Hustadt, U.; Dixon, C.; Fisher, M.; Konev, B.: First-order temporal verification in practice (2005)
- Konev, Boris; Degtyarev, Anatoli; Dixon, Clare; Fisher, Michael; Hustadt, Ullrich: Mechanising first-order temporal resolution (2005)
- Hustadt, Ullrich; Konev, Boris; Riazanov, Alexandre; Voronkov, Andrei: TeMP: A temporal monodic prover (2004)