直觉主义强Löb逻辑的一种新演算：形式化证明的强终止与切割消除
计算机科学中的逻辑
2023-09-04 v1 逻辑
摘要
我们提出了一种新的相继式演算，它对于直觉主义强Löb逻辑 （一种具有可证性解释的直觉主义模态逻辑）具有语法切割消除性质和强终止的反向证明搜索。我们通过对相继式引入一种新的度量，以语法且直接的方式证明了朴素反向证明搜索策略的终止性以及切割的可容许性，从而得到了一个简洁的切割消除过程。所有证明均已在交互式定理证明器 Coq 中形式化。
引用
@article{arxiv.2309.00486,
title = {A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalised},
author = {Ian Shillito and Iris van der Giessen and Rajeev Goré and Rosalie Iemhoff},
journal= {arXiv preprint arXiv:2309.00486},
year = {2023}
}
备注
21-page conference paper + 4-page appendix with proofs