Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions

DOI10.4230/LIPICS.FSCD.2021.11OpenAlexW3184979275MaRDI QIDQ6159926FDOQ6159926

Authors: Kenji Saotome, Koji Nakazawa, Daisuke Kimura 

Publication date: 23 June 2023

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2021/14249/pdf/LIPIcs-FSCD-2021-11.pdf/

Recommendations

• Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• Automated Reasoning with Analytic Tableaux and Related Methods
• Labelled cyclic proofs for separation logic
• A complete cyclic proof system for inductive entailments in first order logic

zbMATH Keywords

linear logicseparation logiccut-eliminationbunched logiccyclic proofs

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx) Computer science (68-XX)

Cited In (2)

• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Restriction on cut rule in cyclic-proof system for symbolic heaps

This page was built for publication: Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions

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