S4及其变体的扭序数演算
计算机科学中的逻辑
2025-01-03 v1
摘要
本文引入并研究了两种用于正常模态逻辑S4的Gentzen风格扭序数演算。所提出的演算不采用否定连接词的标准逻辑推理规则，而是以包含大量否定连接词的可证明否定模态公式的短证明为特征。对这些演算的剪切消除定理进行了证明，同时也获得了这些演算的子公式属性。此外，还考虑了用于其他正常模态逻辑（包括S5）的Gentzen风格扭(超)序数演算。
引用
@article{arxiv.2501.00483,
title = {Twist Sequent Calculi for S4 and its Neighbors},
author = {Norihiro Kamide},
journal= {arXiv preprint arXiv:2501.00483},
year = {2025}
}
备注
In Proceedings NCL'24, arXiv:2412.20053