Instance-Based Theorem Proving with Semantics and Equality

有序语义超链接策略(OSHL)将命题效率、语义和等价性结合在一个集成的一阶逻辑自动定理证明器中。语义是指符号的意义，命题效率是指对需要进行重大案例分析的问题的效率。现有的证明者很少利用语义，而且大多数都不是命题有效的。目前的PROLOG实施将按照最近一篇关于这一主题的论文所建议的方式进行扩展。为了提高速度，方案中还将重新实现证明器。此外，还将实现一个结合了等价性、统一性和命题效率但没有语义的证明器，因为语义可能不总是可用的。在一类重大问题上，这些组合应该会比几乎所有其他证明者表现得更好。还将寻求能够在数百万个输入子句集合上有效证明定理的技术。

The ordered semantic hyper-linking strategy (OSHL) combines propositional efficiency, semantics, and equality in one integrated automatic theorem prover for first-order logic. Semantics refers to the meaning of symbols, and propositional efficiency refers to efficiency on problems requiring significant case analysis. Few existing provers utilize semantics, and most are not propositionally efficient. The current Prolog implementation will be extended in ways that were suggested by a recent paper on the topic. The prover will also be re-implemented in Scheme for greater speed. In addition, a prover combining equality, unification, and propositional efficiency but no semantics will be implemented, because semantics may not always be available. These combinations should outperform almost all other provers on a significant class of problems. Techniques capable of effective theorem proving on sets of millions of input clauses will also be sought.