分离逻辑一个片段中的高效循环蕴含过程
计算机科学中的逻辑
2022-10-04 v1
摘要
高效的蕴含证明系统对于使用分离逻辑的组合验证至关重要。遗憾的是，现有判定过程要么表达力不足要么效率低下。例如，Smallfoot 是一个高效过程，但仅适用于硬编码的链表与树。其他支持一般归纳谓词的过程在时间上呈指数运行，因为其证明搜索需要处理后件中析取带来的回溯。本文提出一种在多项式时间内推导一般归纳谓词循环蕴含证明的判定过程。我们的过程高效且不需要回溯；它使用归一化规则来帮助避免在后件中引入析取。此外，我们的可判定片段具有充分表达力：它基于组合谓词，能够刻画广泛的数据结构，包括有序与嵌套链表段、带快进指针的跳表以及二叉搜索树。我们已在原型工具中实现该方案，并使用近期分离逻辑竞赛中的挑战性问题对其评估。实验结果证实了所提系统的效率。
引用
@article{arxiv.2210.00616,
title = {An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic},
author = {Quang Loc Le and Xuan-Bach D. Le},
journal= {arXiv preprint arXiv:2210.00616},
year = {2022}
}