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

DOI10.1016/0304-3975(87)90129-0zbMath0645.03020MaRDI 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 programs; correctness of a concurrent version of Quicksort; first order temporal logic of linear and discrete time

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Decidability and incompleteness results for first-order temporal logics of linear time, Proof-theoretical investigation of temporal logic with time gaps, Arithmetical axiomatization of first-order temporal logic, Axiomatizing fixpoint logics, Infinitary calculus for a restricted first-order linear temporal logic without contraction on quantified formulas, An approach to infinitary temporal proof theory, Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic, Axiomatising first-order temporal logic: Until and since over linear time, 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