在 $\text{LK}^{\text{h}}$ 中 Skolem 函数的高效消去
逻辑
2022-05-11 v4 计算机科学中的逻辑
摘要
在纯逻辑中消去单个 Skolem 函数仅使证明长度线性增加。该结果针对带有切割的推导证明，这些切割在具有强局部性性质的序列演算中对 Skolem 函数是自由的。
引用
@article{arxiv.1909.01697,
title = {Efficient elimination of Skolem functions in $\text{LK}^{\text{h}}$},
author = {Ján Komara},
journal= {arXiv preprint arXiv:1909.01697},
year = {2022}
}
备注
31 pages; generalization of main results for calculus with cuts, added section on cut elimination, added discussion on eigenvariable condition