束蕴逻辑 BI 可判定性的语法证明
计算机科学中的逻辑
2026-01-06 v4
摘要
束蕴逻辑 BI 为关于资源组合的推理提供了一个框架，并构成了用于推理软件程序的分离逻辑断言语言的基础。命题 BI 通过自由组合命题直觉主义逻辑与乘法直觉主义线性逻辑而得。它具有优雅的证明论：其束蕴演算结合了这两种逻辑的矢列演算。BI 的若干自然扩展已被证明是不可判定的，例如用经典逻辑替换直觉主义逻辑的布尔 BI。这使得 BI 的可判定性尤为引人注目，该性质最近通过复杂的语义论证得以证明。然而，迄今为止，可判定性的语法证明仍然难以捉摸。我们在此使用证明论论证获得了这样一个证明。该证明在技术上很有趣，易于理解，因为它使用常规的束蕴演算（不需要任何 BI 语义的知识），产生了一个可实现的判定过程，并给出了该逻辑复杂度的上界。
引用
@article{arxiv.1609.05847,
title = {A syntactic proof of decidability for the logic of bunched implication BI},
author = {Revantha Ramanayake},
journal= {arXiv preprint arXiv:1609.05847},
year = {2026}
}
备注
Preliminary unpublished draft. Gap in Section 5