束蕴涵逻辑中的聚焦证明搜索
计算机科学中的逻辑
2021-01-27 v2
摘要
束蕴涵逻辑（BI）自由地组合加法与乘法连接词，包括蕴涵；然而，尽管其证明理论已被充分研究，BI 中的证明搜索一直是个困难问题。聚焦原理是对证明搜索空间的一种限制，能够捕捉各种目标导向的证明搜索过程。在本文中，我们通过首先将传统的束序列演算用更简单的嵌套序列数据结构重新表述，进而给出一个极化且聚焦的变体，并通过割消论证证明其可靠且完备，从而表明聚焦证明搜索对 BI 是完备的。这为束蕴涵逻辑中的聚焦证明搜索建立了操作语义。
引用
@article{arxiv.2010.08352,
title = {Focused Proof-search in the Logic of Bunched Implications},
author = {Alexander Gheorghiu and Sonia Marin},
journal= {arXiv preprint arXiv:2010.08352},
year = {2021}
}
备注
18 pages content