zbMATH — the first resource for mathematics

Investigation on fragments of first order branching temporal logic. (English) Zbl 1002.03016
Various fragments of first-order computational tree logic (FOCTL) are investigated. The fragment of the logic with only the operator F (sometimes in the future) is not axiomatizable. This is shown by a possible embedding of arithmetic into it. The proof can be extended to first-order linear time logic. It is also proved that the logic with the past operator H (always in the past) is not axiomatizable as well. The proof is done by showing that the set of valid formulae of \(\mathbf{FOCTL}_{\mathbf H}\) is \(\Pi^0_2\)-complete. The only axiomatizable fragment is the one with the next operator (X).

03B44 Temporal logic
03B25 Decidability of theories and sets of sentences
03B70 Logic in computer science
Full Text: DOI
[1] Alur, Information and Computation 104 pp 35– (1993)
[2] and , Logics and models of real time: A Survey. In: Real Time: Theory in Practice, Lecture Notes in Computer Science 600, Springer Verlag, Berlin-Heidelberg-New York 1992, pp. 74 126.
[3] The Power of Temporal Proofs. Ph. D. Thesis, Stanford University 1988.
[4] and , Computability and Logic. Cambridge University Press, Cambridge 1974.
[5] Temporal and Modal Logic. In: H and book of Theoretical Computer Science, Volume B, Elsevier, Amsterdam 1990. · Zbl 0900.03030
[6] Emerson, J. ACM 33 pp 151– (1986)
[7] Quantification in modal logic. In: H and book of Philosophical Logic, Volume II, D. Reidel Publishing Comp., Dordrecht 1984, pp. 249 - 307. · Zbl 0875.03050
[8] , and , Temporal Logic: Mathematical Foundation and Computational Aspects, Volume 1. Clarendon Press, Oxford 1994.
[9] Szalas, Theoret. Comp. Sci. 47 pp 329– (1986)
[10] Temporal logic. In: H and book of Logic in Artificial Intelligence and Logic Programming, Volume 4, Clarendon Press, Oxford 1995, pp. 241 - 350.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.