Inductive Completeness of Logics of Programs

DOI10.1016/J.ENTCS.2008.12.119zbMath1234.03018OpenAlexW1977335112MaRDI QIDQ2804944

Daniel Leivant

Publication date: 6 May 2016

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.119

zbMATH Keywords

Hoare logicprogram semanticsinductive definitionsinductive completeness

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

On the Completeness of Dynamic Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic
• Programs and program verifications in a general setting
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Termination assertions for recursive programs: Completeness and axiomatic definability
• Diamond formulas: A fragment of dynamic logic with recursively enumerable validity problem
• Axiomatic Definitions of Programming Languages
• Soundness and Completeness of an Axiom System for Program Verification
• Reasoning in Dynamic Logic about Program Termination

This page was built for publication: Inductive Completeness of Logics of Programs