Pages that link to "Item:Q5200020"
From MaRDI portal
The following pages link to Automated Cyclic Entailment Proofs in Separation Logic (Q5200020):
Displaying 24 items.
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs (Q1798782) (← links)
- Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps (Q2039937) (← links)
- Non-well-founded deduction for induction and coinduction (Q2055840) (← links)
- Cyclic proofs, hypersequents, and transitive closure logic (Q2104539) (← links)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- Automated mutual induction proof in separation logic (Q2414251) (← links)
- Completeness and expressiveness of pointer program verification by separation logic (Q2417849) (← links)
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints (Q2817951) (← links)
- Cyclic Arithmetic Is Equivalent to Peano Arithmetic (Q2988374) (← links)
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System (Q2988375) (← links)
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic (Q2988661) (← links)
- Completeness for a First-Order Abstract Separation Logic (Q3179309) (← links)
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives (Q3454118) (← links)
- A First-Order Logic with Frames (Q5041109) (← links)
- (Q5111651) (← links)
- (Q5208872) (← links)
- (Q5227521) (← links)
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions (Q5875940) (← links)
- Program Verification with Separation Logic (Q5883571) (← links)
- Cyclic hypersequent system for transitive closure logic (Q6050767) (← links)
- Completeness of cyclic proofs for symbolic heaps with inductive definitions (Q6536318) (← links)
- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points (Q6541152) (← links)
- Restriction on cut rule in cyclic-proof system for symbolic heaps (Q6633582) (← links)
- Abstract cyclic proofs (Q6646012) (← links)