Restriction on cut rule in cyclic-proof system for symbolic heaps
type: Item
instance of: scholarly article
title: Restriction on cut rule in cyclic-proof system for symbolic heaps
author: Kenji Saotome
author: Koji Nakazawa
author: Daisuke Kimura
published in: Theoretical Computer Science
publication date: 2024-11-06T00:00:00Z
Mathematics Subject Classification ID: 68Qxx
zbMATH DE Number: 7939425
zbMATH Keywords: cyclic-proof system
zbMATH Keywords: separation logic
zbMATH Keywords: symbolic heap
zbMATH Keywords: cut elimination
MaRDI profile type: Publication
cites work: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
cites work: Programming Languages and Systems
cites work: Foundations for Decision Problems in Separation Logic with General Inductive Predicates
cites work: The Tree Width of Separation Logic with Recursive Definitions
cites work: Deciding Entailments in Inductive Separation Logic with Tree Automata
cites work: Compositional Invariant Checking for Overlaid and Nested Linked Lists
cites work: Compositional Entailment Checking for a Fragment of Separation Logic
cites work: Tractable Reasoning in a Fragment of Separation Logic
cites work: Completeness of cyclic proofs for symbolic heaps with inductive definitions
cites work: A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
cites work: Automated Cyclic Entailment Proofs in Separation Logic
cites work: Sequent calculi for induction and infinite descent
cites work: Formalised Inductive Reasoning in the Logic of Bunched Implications
cites work: Automated mutual explicit induction proof in separation logic
cites work: Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions
cites work: Q4032549
cites work: Q4559476
cites work: A proof procedure for separation logic with inductive definitions and data
cites work: Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
DOI: 10.1016/J.TCS.2024.114854
description: scientific article; zbMATH DE number 7939425