M.L. Bonet 与 S.R. Buss 的 Frege 系统证明模拟程序的推广
逻辑
2024-03-15 v1 计算机科学中的逻辑
摘要
在本文中，我们将 Bonet 和 Buss 针对 Frege 系统的证明模拟程序推广至一些演绎定理不成立的逻辑。特别地，我们研究了有限值 Łukasiewicz 逻辑的情形。为此，我们提供了证明系统，这些系统分别用析取消去规则的嵌套版本和一般版本扩充了 Avron 针对 Łukasiewicz 三值逻辑的 Frege 系统。对于这些系统，我们给出了关于证明步数和证明长度的加速上界。我们还考虑了 Tamminga 的自然演绎和 Avron 针对 3 值 Łukasiewicz 逻辑的超继演算，并将我们关于析取消去规则的结果推广至所有有限值 Łukasiewicz 逻辑。
引用
@article{arxiv.2403.09119,
title = {Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss},
author = {Daniil Kozhemiachenko},
journal= {arXiv preprint arXiv:2403.09119},
year = {2024}
}