A sequent calculus for trace formula implication

DOI10.1007/978-3-032-06085-3_25MaRDI QIDQ6860367zbMATH OpenFDO

Authors Niklas Heidler, Reiner Hähnle

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-06085-3_25

zbMATH Keywords

\( \mu \)-calculusfixed point logicprogram specification

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• An axiomatic basis for computer programming
• Deductive software verification: from pen-and-paper proofs to industrial tools
• scientific article; zbMATH DE number 3848604 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1304336 (Why is no real title available?)
• scientific article; zbMATH DE number 1536570 (Why is no real title available?)
• scientific article; zbMATH DE number 2087435 (Why is no real title available?)
• On Context-Free Languages
• On global induction mechanisms in aμ-calculus with explicit approximations
• Trace-Based Coinductive Operational Semantics for While

This page was built for publication: A sequent calculus for trace formula implication

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