The power of temporal proofs

DOI10.1016/0304-3975(89)90138-2zbMath0669.03010OpenAlexW2024016985MaRDI QIDQ1118578

Martín Abadi

Publication date: 1989

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

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90138-2

zbMATH Keywords

auxiliary definitionsaxiomatic system complete with respect to nonstandard models of FTLfirst order temporal logic

Mathematics Subject Classification ID

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

Related Items (20)

The power of the ``always operator in first-order temporal logic ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ Programming in metric temporal logic ⋮ A propositional probabilistic logic with discrete linear time for reasoning about evidence ⋮ Temporal abductive reasoning about biochemical reactions ⋮ Multi-dimensional logic programming: theoretical foundations ⋮ Specification of abstract dynamic-data types: A temporal logic approach ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Theorem proving using clausal resolution: from past to present ⋮ A decidability result for the model checking of infinite-state systems ⋮ Foundations of linear-time logic programming ⋮ Temporal logics need their clocks ⋮ Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics ⋮ Decidability of infinite-state timed CCP processes and first-order LTL ⋮ LTL over integer periodicity constraints ⋮ Temporal prophecy for proving temporal properties of infinite-state systems ⋮ Linear-time temporal logics with Presburger constraints: an overview ★ ⋮ Similarity saturation for first order linear temporal logic with UNLESS ⋮ On the strength of temporal proofs

Cites Work

• Adequate proof principles for invariance and liveness properties of concurrent programs
• The temporal semantics of concurrent programs
• Axioms for tense logic. II: Time periods
• Provability interpretations of modal logic
• Proving Liveness Properties of Concurrent Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The power of temporal proofs