On the strength of temporal proofs
From MaRDI portal
Publication:809066
DOI10.1016/0304-3975(91)90386-GzbMath0732.03020MaRDI QIDQ809066
Istvan Németi, Ildikó Sain, Hajnalka Andréka
Publication date: 1991
Published in: Theoretical Computer Science (Search for Journal in Brave)
03B45: Modal logic (including the logic of norms)
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Derivation rules as anti-axioms in modal logic, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, Temporal logics need their clocks, 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
