Incompleteness of first-order temporal logic with until
The version of first-order temporal logic (with equality) chosen in this paper is essentially that introduced by \textit{Z. Manna} and \textit{A. Pnueli} [Verification of concurrent programs: the temporal framework, in: The correctness problem in computer science (\textit{R. S. Boyer} and \textit{J S. Moore} (eds.)), 215-273 (1981; Zbl 0476.68009)]; it uses the temporal modalities ``always, ``sometimes, ``next time, ``until and ``at next. It is shown that this logic is weakly incomplete (the set of tautologies over an arbitrary signature is not r.e.) and strongly incomplete (the set of tautologies is r.e. for no signature). Although the first claim is a consequence of the second, they are separately presented. The proof of the first theorem is analogous to the proof of incompleteness of second-order prediate logic. It is based on Trakhtenbrot's theorem and the fact that finite structures are characterizable in temporal logic (this result is interesting by its own). For the second theorem, the technique consists in reducing the complement of the halting problem for Turing machines to the problem whether a temporal formula (only with \(``=)\) is a tautology.
- scientific article; zbMATH DE number 3968560
- Decidability and incompleteness results for first-order temporal logics of linear time
- On the strength of temporal proofs
- Temporal logics need their clocks
- scientific article; zbMATH DE number 3972843
- scientific article; zbMATH DE number 1678387
- Decidable fragments of first-order temporal logics
- scientific article; zbMATH DE number 4053579
- Concerning the semantic consequence relation in first-order temporal logic
- Axiomatising first-order temporal logic: Until and since over linear time
- Concerning the semantic consequence relation in first-order temporal logic
- Arithmetical axiomatization of first-order temporal logic
- A complete axiomatic characterization of first-order temporal logic of linear time
- Expressive completeness failure in branching time structures
- The power of temporal proofs
- Completeness of a first-order temporal logic with time-gaps
- Specification of abstract dynamic-data types: A temporal logic approach
- Decidable fragments of first-order temporal logics
- Equality and monodic first-order temporal logic
- A decision procedure and complete axiomatization for projection temporal logic
- Parameterized verification of leader/follower systems via first-order temporal logic
- On strictly arithmetical completeness in logics of programs
- Mechanising first-order temporal resolution
- Incompleteness in linear time
- Kripke incompleteness of first-order calculi with temporal modalities of CTL and near logics
- Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
- scientific article; zbMATH DE number 3858393 (Why is no real title available?)
- On temporal logics with data variable quantifications: decidability and complexity
- scientific article; zbMATH DE number 4053579 (Why is no real title available?)
- Decidability and incompleteness results for first-order temporal logics of linear time
- A decidability result for the model checking of infinite-state systems
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
- Similarity saturation for first order linear temporal logic with UNLESS
- Axioms for real-time logics
- Incompleteness of a first-order Gödel logic and some temporal logics of programs
- Trakhtenbrot theorem and first-order axiomatic extensions of MTL
- On the interpretability of arithmetic in temporal logic
This page was built for publication: Incompleteness of first-order temporal logic with until
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1123184)
