Schuette 模式下直觉主义逻辑的多后件相继式演算中的证明搜索
逻辑
2017-01-04 v5
摘要
遵循 G. Mints (Kluwer 2000 及 2013 年草稿) 的工作,我们以 Schuette 模式的精神,提出了针对直觉主义命题逻辑、直觉主义谓词逻辑片段以及完整直觉主义谓词逻辑的多后件相继式演算中的终止且双完备的证明搜索方法。
引用
@article{arxiv.1312.1136,
title = {Proof search in multi-succedent sequent calculi for intuitionistic logic under the Schuette's schema},
author = {Toshiyasu Arai},
journal= {arXiv preprint arXiv:1312.1136},
year = {2017}
}