Decidability and incompleteness results for first-order temporal logics of linear time
- 1 January 1992
- journal article
- research article
- Published by Taylor & Francis in Journal of Applied Non-Classical Logics
- Vol. 2 (2) , 139-156
- https://doi.org/10.1080/11663081.1992.10510779
Abstract
The question of axiomatizability of first-order temporal logics is studied w.r.t. different semantics and several restrictions on the language. The validity problem for logics admitting flexible interpretations of the predicate symbols or allowing at least binary predicate symbols is shown to be Π1 1-complete. In contrast, it is decidable for temporal logics with rigid monadic predicate symbols but without function symbols and identity.Keywords
This publication has 11 references indexed in Scilit:
- On the interpretability of arithmetic in temporal logicTheoretical Computer Science, 1990
- Nonclausal deduction in first-order temporal logicJournal of the ACM, 1990
- The power of temporal proofsTheoretical Computer Science, 1989
- Temporal Logic Programming is Complete and Expressive,Published by Defense Technical Information Center (DTIC) ,1988
- Incompleteness of first-order temporal logic with untilTheoretical Computer Science, 1988
- A complete axiomatic characterization of first-order temporal logic of linear timeTheoretical Computer Science, 1987
- Concerning the semantic consequence relation in first-order temporal logicTheoretical Computer Science, 1986
- Synthesis of Communicating Processes from Temporal Logic SpecificationsACM Transactions on Programming Languages and Systems, 1984
- Propositional dynamic logic of nonregular programsJournal of Computer and System Sciences, 1983
- Temporal logic can be more expressiveInformation and Control, 1983