Name
Abstract | ||
|---|---|---|
It has been shown that some variants of cyclic proof systems for symbolic heap entailments in separation logic do not enjoy the cut elimination property. To construct complete system, we have to consider the cut rule, which requires some heuristics to find cut formulas in bottom-up proof search. Hence, we hope to achieve some restricted variant of cut rule which does not change provability and does not interfere with automatic proof search without heuristics. This paper gives a limit on this challenge. We propose a restricted cut rule, called the presumable cut, in which cut formula is restricted to those which can occur below the cut. This paper shows that there is an entailment which is provable with full cuts in cyclic proof system for symbolic heaps, but not with only presumable cuts. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-59025-3_6 | FLOPS |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kenji Saotome | 1 | 0 | 0.34 |
| Koji Nakazawa | 2 | 36 | 6.92 |
| Daisuke Kimura | 3 | 5 | 2.14 |