A complete axiomatic characterization of first-order temporal logic of linear time

DOI10.1016/0304-3975(87)90129-0zbMath0645.03020OpenAlexW2074329619WikidataQ127491328 ScholiaQ127491328MaRDI QIDQ1102941

Andrzej Szałas

Publication date: 1987

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(87)90129-0

zbMATH Keywords

concurrent programscorrectness of a concurrent version of Quicksortfirst order temporal logic of linear and discrete time

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (14)

The logic of ``initially and ``next: complete axiomatization and complexity ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ Arithmetical axiomatization of first-order temporal logic ⋮ A note on infinitary continuous logic ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ Axiomatizing fixpoint logics ⋮ Proof-theoretical investigation of temporal logic with time gaps ⋮ An approach to infinitary temporal proof theory ⋮ Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic ⋮ Similarity saturation for first order linear temporal logic with UNLESS ⋮ Axiomatising first-order temporal logic: Until and since over linear time ⋮ Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas ⋮ Invertible infinitary calculus without loop rules for restricted FTL ⋮ Replacement of Induction by Similarity Saturation in a First Order Linear Temporal Logic

Cites Work

• A generalized nexttime operator in temporal logic
• Concerning the semantic consequence relation in first-order temporal logic
• Arithmetical axiomatization of first-order temporal logic
• Incompleteness of first-order temporal logic with until
• Completeness Proofs for Some Logics of Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A complete axiomatic characterization of first-order temporal logic of linear time