z3 - 我们可以在 Z3 中设计关于分离逻辑的推理规则并用它来自动证明一些 props 吗？

Question

我们可以在 z3 中设计关于分离逻辑的推理规则和公理，并用它来自动证明一些 props 吗？例如，“x=y /\ (x |-> z) |- x=y /\ (y |-> z)”

Answer 1

可能。多个小组正在研究基于 SMT 求解器或与它们集成的分离逻辑证明器。以下是有关该主题的一些最新出版物：

Ruzica Piskac、Thomas Wies、Damien Zufferey：使用 SMT 自动化分离逻辑。2013 年

Matko Botincan、Matthew J. Parkinson、Wolfram Schulte：使用 SMT 求解器对 C 程序进行分离逻辑验证。电。笔记理论。计算。科学。254

Juan Antonio Navarro Pérez，Andrey Rybalchenko：分离逻辑模理论。APLAS 2013

我敢肯定还有很多其他的 SL 证明者，但我知道的一个是SLAyer。