Inductive completeness of logics of programs

DOI10.1016/J.ENTCS.2008.12.119MaRDI QIDQ2804944zbMATH OpenOpenAlexFDO

Authors Daniel M. 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

program semanticsHoare logicinductive definitionsinductive completeness

Mathematics Subject Classification ID

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

Recommendations

• On the Completeness of Dynamic Logic
• Effective Axiomatizations of Hoare Logics
• Two theorems about the completeness of Hoare's logic
• Logic programs as specifications in the inductive verification of logic programs
• A completeness theorem for dynamic logic

Cites work

• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1860676 (Why is no real title available?)
• scientific article; zbMATH DE number 3237808 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3346319 (Why is no real title available?)
• scientific article; zbMATH DE number 3365218 (Why is no real title available?)
• An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic
• Axiomatic Definitions of Programming Languages
• Diamond formulas: A fragment of dynamic logic with recursively enumerable validity problem
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Programs and program verifications in a general setting
• Reasoning in Dynamic Logic about Program Termination
• Soundness and Completeness of an Axiom System for Program Verification
• Termination assertions for recursive programs: Completeness and axiomatic definability

Cited in

(9)

• Weak arithmetic completeness of object-oriented first-order assertion networks
• scientific article; zbMATH DE number 1223543 (Why is no real title available?)
• Well-definedness and observational equivalence for inductive–coinductive programs
• On the Completeness of Dynamic Logic
• Inductive expansion: A calculus for verifying and synthesizing functional and logic programs
• An almost machine-independent theory of program-length complexity, sophistication, and induction
• Reasoning About Incompletely Defined Programs
• scientific article; zbMATH DE number 3952736 (Why is no real title available?)
• Checking Sufficient Completeness by Inductive Theorem Proving

This page was built for publication: Inductive completeness of logics of programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804944)