论文标题
集中的证明搜索逻辑的逻辑
Focused Proof-search in the Logic of Bunched Implications
论文作者
论文摘要
束含义的逻辑（BI）自由地结合了添加剂和乘法连接剂，包括含义；但是，尽管有充分的证明理论，但BI中的证明搜索一直是一个困难的问题。聚焦原则是对验证空间的限制，可以捕获各种目标指导的证明搜索程序。在本文中，我们表明，通过首先使用嵌套序列的更简单的数据结构来重新构造传统的串联序列微积分，这是BI的完整搜索，然后使用偏光化和专注的变体，我们证明，通过切割淘汰的论证，我们证明了这一点。这建立了一种操作语义，用于以束缚含义的逻辑进行重点证明搜索。
The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper, we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications.
