On the strength of temporal proofs

DOI10.1016/0304-3975(91)90386-GzbMath0732.03020OpenAlexW1571059814MaRDI QIDQ809066

Hajnalka Andréka, Istvan Németi, Ildikó Sain

Publication date: 1991

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

Full work available at URL: https://doi.org/10.1016/0304-3975(91)90386-g

zbMATH Keywords

temporal logicscorrectness assertions

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 (6)

Derivation rules as anti-axioms in modal logic ⋮ A propositional probabilistic logic with discrete linear time for reasoning about evidence ⋮ Temporal logics need their clocks ⋮ On the axiomatizability of some first-order spatio-temporal theories ⋮ Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics ⋮ Lambek calculus and its relational semantics: Completeness and incompleteness

Cites Work

• Total correctness in nonstandard logics of programs
• A completeness theorem for dynamic logic
• A simple proof for the completeness of Floyd's method
• An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic
• Cylindric algebras. Part II
• Non-standard algorithmic and dynamic logic
• The power of temporal proofs
• Weak second order characterizations of various program verification systems
• A complete logic for reasoning about programs via nonstandard model theory. II
• Programs and program verifications in a general setting
• Determinateness of program equivalence over peano axioms
• Temporal logics need their clocks
• First-order dynamic logic
• Handbook of philosophical logic. Vol. 9
• Recursive programs and denotational semantics in absolute logics of programs
• STRUCTURED NONSTANDARD DYNAMIC LOGIC
• A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
• On the termination of program schemas
• To the memory of Arthur Prior Formal properties of ‘now’
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the strength of temporal proofs