由截断谓词演算公理生成定理证明过程
计算机科学中的逻辑
2019-07-31 v1
摘要
我们提出了一种解决自动定理证明问题的新方法。基于一组所谓截断谓词演算（标准谓词演算的子集）的公理，生成了用于识别属于某一理论的句子的多项式代价过程。文中包含了若干示例问题以展示所提方法的性能。
引用
@article{arxiv.1907.12636,
title = {Generating theorem proving procedures from axioms of Truncated Predicate Calculus},
author = {Grzegorz Wiaderek and Iwona Skalna},
journal= {arXiv preprint arXiv:1907.12636},
year = {2019}
}