Equivalences among logics of programs

DOI10.1016/0022-0000(84)90027-8zbMath0552.68037OpenAlexW1978823961MaRDI QIDQ801684

Albert R. Meyer, Jerzy Tiuryn

Publication date: 1984

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(84)90027-8

zbMATH Keywords

determinismdynamic logicnondeterminismalgorithmic logicdeterministic effective flowchartseffective definitional schemesfirst-order logics of programslogic of effective definitionsnondeterministic effective flowcharts

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items

``During cannot be expressed by ``after, Some relationships between logics of programs and complexity theory, A simplified proof of \(DDL<DL\), Computational inductive definability, A logic of recursion

Cites Work

• Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. I
• Definability in dynamic logic
• Expressing program looping in regular dynamic logic
• Theory of program structures: Schemes, semantics, verification
• Finiteness is mu-ineffable
• First-order dynamic logic
• Deterministic dynamic logic is strictly weaker than dynamic logic
• Axiomatic Definitions of Programming Languages
• Algorithmic properties of structures
• Remarks on an infinitary language with constructive formulas
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item