Coq 中形式化的 bunched implications 逻辑的语义切消

bunched implications 逻辑（BI）是一种子结构逻辑，构成了分离逻辑的基础，而分离逻辑是用于推理堆操作程序的被广泛研究的逻辑。尽管 BI 的证明理论与元理论在数学上十分复杂，重要元理论结果的形式化仍很初步。在本文中，我们给出了在 Coq 证明助手中形式化的、自包含的 BI 一个核心元理论性质的证明：其相继式演算的切消。所给出的证明是*语义的*，意即通过在一个特定的“泛”模型中解释相继式而得到。这产生了比标准的 Gentzen 式切消论证更模块化且更优雅的证明，而后者在 BI 的手动证明中往往微妙且易错。特别地，我们的语义方法避免了对证明推导的不必要逆规则，或切归约与多切规则的使用。除了模块化，我们的方法也很稳健：我们展示了我们的方法如何以微小修改扩展到（i）带有任意一组\emph{简单结构规则}的 BI 扩展，以及（ii）带有类 S4 的 $\Box$ 模态的扩展。