基于自然演绎界限的相继式演算证明搜索过程与反模型生成
计算机科学中的逻辑
2020-02-04 v4
摘要
在先前发表的 ENTCS 论文（Santos 等人（2016））中，我们引入了称为 的极小蕴涵命题逻辑（）的相继式演算。该演算为 提供了一种自底向上的证明搜索过程。我们证明了 的可靠性与完备性。我们还提出了一种保证证明搜索过程终止的策略。在本论文中，我们精炼了该策略并给出了 终止的新策略。考虑此新策略，我们还提供了系统的（新）完备性证明，改进了先前版本。此外，我们给出了由此新策略导出的证明搜索过程的显式上界。我们也提供了系统的完整可靠性证明。
引用
@article{arxiv.1905.02059,
title = {A Sequent Calculus Proof Search Procedure and Counter-model Generation based on Natural Deduction Bounds},
author = {Jefferson de Barros Santos and Bruno Lopes Vieira and Edward Hermann Haeusler},
journal= {arXiv preprint arXiv:1905.02059},
year = {2020}
}