The flower calculus

DOI10.4230/LIPICS.FSCD.2024.5MaRDI QIDQ6875012zbMATH OpenFDO

Authors Pablo Donato

Publication date 14 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2024.5

zbMATH Keywords

cut-eliminationdeep inferenceexistential graphsgraphical calculiintuitionistic logicKripke semantics

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A categorical interpretation of C. S. Peirce's propositional logic Alpha
• A fully automatic theorem prover with human-style output
• A graphical deep inference system for intuitionistic logic
• A Local System for Intuitionistic Logic
• An intuitionistic formula hierarchy based on high‐school identities
• Annotation-free sequent calculi for full intuitionistic linear logic
• Automated generation of illustrated proofs in geometry and beyond
• Automating Coherent Logic
• Compositional Diagrammatic First-Order Logic
• Equivalence proof for intuitionistic existential alpha graphs
• From axioms to synthetic inference rules via focusing
• scientific article; zbMATH DE number 2185694 (Why is no real title available?)
• scientific article; zbMATH DE number 1479613 (Why is no real title available?)
• scientific article; zbMATH DE number 1773524 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 7699421 (Why is no real title available?)
• Intuitionistic S4 is decidable
• Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen.
• Maehara-style modal nested calculi
• Modular focused proof systems for intuitionistic modal logics
• Nested sequents for intuitionistic logics
• Nested sequents for intuitionistic modal logics via structural refinement
• On a graph calculus for modalities
• On graph calculi for multi-modal logics
• On graph reasoning
• PDL for structured data: a graph-calculus approach
• Peirce's logic of continuity: existential graphs and non-Cantorian continuum
• Preface. A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday
• Proof analysis of Peirce's alpha system of graphs
• Proofs with graphs
• Sequential calculus
• Spider Diagrams
• Subformula Linking as an Interaction Method
• Subformula linking for intuitionistic logic with application to type theory
• The flower calculus
• The Lean 4 theorem prover and programming language
• The use of machines to assist in rigorous proof
• Topological representations of distributive lattices and Brouwerian logics
• Typed Lambda Calculi and Applications

Cited in

(1)

• The flower calculus

This page was built for publication: The flower calculus

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