能否在Z3中设计关于分离逻辑的推理规则，并用它来自动证明一些道具?

Question

能否在z3中设计关于分离逻辑的推理规则和公理，并用它来自动证明一些道具?例如,"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年Sci。

Juan Antonio Navarro p兼并，Andrey Rybalchenko:分离逻辑模理论。APLAS 2013

我相信还有很多其他的SL证明器，但我知道的一个是SLAyer。