Inductive completeness of logics of programs

DOI10.1016/J.ENTCS.2008.12.119zbMATH Open1234.03018OpenAlexW1977335112MaRDI QIDQ2804944FDOQ2804944

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

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

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)

Cites Work

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

Cited In (8)

• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• 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)