Restriction on Cut in Cyclic Proof System for Symbolic Heaps
Restriction on Cut in Cyclic Proof System for Symbolic Heaps
复制标题
符号堆循环证明系统中剪切的限制
DOI：
10.1007/978-3-030-59025-3_6
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Kimura Daisuke
中科院分区：
文献类型：
--
作者：
Saotome Kenji;Nakazawa Koji;Kimura Daisuke
证明了分离逻辑中用于符号堆蕴涵的循环证明系统的某些变体不具有割消元性质。为了构建完整的系统，我们必须考虑割集规则，这需要一些启发式方法来寻找自底向上的证明搜索中的割集公式。因此，我们希望在不改变可证明性和不干扰自动证明搜索而不使用启发式的情况下，实现切割规则的某种受限变体。这篇论文对这一挑战进行了限制。我们提出了一个限制切割规则，称为假定切割，其中切割公式被限制在切割下可能出现的那些。本文证明了在符号堆的循环证明系统中存在一个完全割可证的蕴涵，而不是只有假定割。
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.
登录
查看更多内容
16 值推理的免割系统
DOI：
--
发表时间：
2005
期刊：
Bulletin of the Section of Logic 34(4)
影响因子：
--
作者：
上出哲広;上出哲広;上出哲広;上出哲広;上出哲広;上出哲広;上出哲広
通讯作者：
上出哲広
（克莱恩行动）的非充分证明理论（代数格）
DOI：
10.4230/lipics.csl.2018.19
发表时间：
2018
期刊：
ArXiv
影响因子：
--
作者：
Anupam Das;D. Pous
通讯作者：
D. Pous
通用循环定理证明者
影响因子：
0.6
作者：
J. Brotherston;Nikos Gorogiannis;R. Petersen
通讯作者：
R. Petersen
具有归纳定义的符号堆循环证明的完整性
DOI：
10.1007/978-3-030-34175-6_19
发表时间：
2019
期刊：
LNCS (APLAS 2019)
影响因子：
--
作者：
Tatsuta Makoto;Nakazawa Koji;Kimura Daisuke
通讯作者：
Kimura Daisuke
分离逻辑循环证明中割消除的失败
DOI：
--
发表时间：
2019
期刊：
影响因子：
--
作者：
Daisuke Kimura;Koji Nakazawa;Tachio Terauchi;and Hiroshi Unno
通讯作者：
and Hiroshi Unno