实现Labeled Sequent Calculi for Tense Logics的最大分析显示片段

我们定义并研究了最大化分析显示计算器体系与标记序言计算器体系之间的翻译，从而解决了关于两种形式化方法之间证明可译性的开放问题。特别是，我们提供了将无剪切显示证明映射到和从称为‘严格’的标记证明之间的 PTIME 翻译。这将无剪切显示证明空间与标记证明中一个多项式等价的子空间相互关联，表明两种形式化方法在多项式时间内相互模拟。我们分析了在该翻译下证明大小的相对情况，发现显示证明在翻译为严格标记证明时变得多项式缩短，尽管可能增加序言的长度；在相反的翻译中，严格标记证明在翻译为显示证明时可能变得多项式更大。为实现我们的成果，我们以新的方式将标记序言计算器体系形式化，将规则视为‘模板’，通过替换来获得规则应用；我们还提供了在标记序言形式化中定义原初时态结构规则的第一个定义。因此，我们的标记计算器体系更接近于为时态逻辑定义的显示计算器体系，这允许更细致地分析规则、替换和翻译。本工作表明，针对时态逻辑的每个分析显示计算器体系都可以被视为标记序言计算器体系，从而确凿地表明标记形式化方法在原始时态逻辑的语境下包含并扩展了显示形式化方法。