索引嵌套推理的句法消除的诱导
摘要：逻辑的证明论研究的关键是具有子公式属性的证明演算。为了为许多感兴趣的逻辑提供这样的演算，引入了许多不同的证明形式（如序列、嵌套序列、标记序列形式）。最近，将嵌套序列形式推广为索引嵌套序列，以产生对(K的模态逻辑的扩展的(Lemmon-Scott) Geach公理具有子公式属性的证明演算。其中的完备性和去切引理是语义的和复杂的。这里我们展示了标记序列形式的推导，其中的序列"几乎类似于树状"与索引嵌套序列完全对应。利用这种对应关系，我们可以利用现有的标记序列演算中存在的优雅证明来产生索引嵌套序列演算的句法证明。这项工作的一个更大目标是展示如何专门化现有的证明转换，从而减轻在每个形式中独立证明的需要。这种变换还可以用来引出新的无割演算。我们利用这一点介绍了中间逻辑的第一个索引嵌套序列演算。
作者：Revantha Ramanayake
论文ID：1703.01356
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22