Investigation on fragments of first order branching temporal logic

DOI10.1002/1521-3870(200201)48:1%3C51::AID-MALQ51%3E3.0.CO;2-SMaRDI QIDQ2776809zbMATH OpenOpenAlexFDO

Authors Franco Montagna, G. Michele Pinna, Elisa B. P. Tiezzi

Publication date 7 January 2003

Published in Mathematical Logic Quarterly (MLQ) (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/1521-3870(200201)48:1%3C51::aid-malq51%3E3.0.co;2-s

zbMATH Keywords

axiomatizationfirst-order branching temporal logicFOCTL

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Logic in computer science (03B70)

Review text

Various fragments of first-order computational tree logic (\textbf{FOCTL}) are investigated. The fragment of the logic with only the operator \textbf{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 \textbf{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 (\textbf{X}).

Recommendations

• First-order logics of braching time: on expressive power of temporal operators
• scientific article; zbMATH DE number 5790393
• Axiomatizing the monodic fragment of first-order temporal logic
• Decidable fragments of first-order temporal logics
• Decidability and incompleteness results for first-order temporal logics of linear time

Cited in

(4)

• Obituary: Franco Montagna (1948--2015)
• First-order logics of braching time: on expressive power of temporal operators
• Axiomatizing the Monodic Fragment of
• The modal logic of potential infinity: branching versus convergent possibilities

This page was built for publication: Investigation on fragments of first order branching temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2776809)