关于霍尔逻辑相对于标准模型的完备性结果
计算机科学中的逻辑
2017-03-02 v1
摘要
霍尔逻辑相对于皮亚诺算术标准模型的一般完备性问题已由 Cook 研究，它允许使用任意算术公式作为断言。在实践中，断言会是简单的算术公式，例如算术层次中较低层次的公式。此外，我们发现，通过将输入限制到，保持霍尔逻辑完备性所需的最小断言理论的复杂度可以降低。本文通过限制断言为算术公式的子类（并通过将输入限制到）进一步研究霍尔逻辑相对于的完备性。我们的完备性结果通过降低断言理论的复杂度改进了 Cook 的结果。
引用
@article{arxiv.1703.00237,
title = {On Completeness Results of Hoare Logic Relative to the Standard Model},
author = {Zhaowei Xu and Wenhui Zhang and Yuefei Sui},
journal= {arXiv preprint arXiv:1703.00237},
year = {2017}
}