分离谷物与chaff: 理解证明机制的(不)完备性——针对带归纳定义的分离逻辑
计算机科学中的逻辑
2025-12-05 v2 编程语言
摘要
对于两十多年来，分离逻辑（Separation Logic）已成为最流行的框架之一，用于推理处理堆操作程序以及共享资源和权限。分离逻辑常被扩展以包括归纳定义的谓词，解释为最小固定点，形成带归纳定义的分离逻辑（SLID）。在开发自动化证明机制以SLID方面，已取得许多理论和实际进展，但这些机制并非完美，深入理解其失败的原因仍是迫切需求。正如人们所熟知的，分离逻辑并非完备，事实上，它包含了若干无法被自动推理的完备性来源。本文研究了这些完备性来源及其与证明机制失败之间的关系。我们将SLID置于更大的逻辑中，我们称为弱分离逻辑（WSL）。我们证明了与SLID不同，WSL对于带有背景理论和归纳定义的量化包含式的一个非平凡片段是完备的，通过归约到一阶逻辑（FOL）。此外，我们展示了常见的折叠/展开证明机制对于无理论、无量化的WSL包含式与归纳定义是 sound 且 complete 的。通过这一点，我们将证明失败理解为源于WSL中但不允许于SLID的非标准模型。这些rogue模型通常是无限的，我们使用符号结构来表示和自动发现它们。我们 presenting 一个原型工具，其实现了WSL的FOL编码并在现有基准测试上进行测试，其中包含超过700个带有归纳定义的量化包含问题。我们的工具能够发现许多示例的反模型，我们提供一种对rogue模型的部分分类，为理解现实世界的证明失败提供了一些启示。
引用
@article{arxiv.2511.20193,
title = {Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions},
author = {Neta Elad and Adithya Murali and Sharon Shoham},
journal= {arXiv preprint arXiv:2511.20193},
year = {2025}
}