Instance-Based Theorem Proving with Semantics and Equality

有序语义超链接策略（OSHL）将命题效率、语义和等式结合在一个一阶逻辑的集成自动定理证明器中。 语义是指符号的意义，命题效率是指对需要重要案例分析的问题的效率。 很少有现有的证明器利用语义，大多数都不是命题效率。 当前的Prolog实现将以最近一篇关于该主题的论文所建议的方式进行扩展。 为了更快的速度，还将在Scheme中重新实现该校准器。 此外，将实现一个结合了等式、统一和命题效率但没有语义的证明器，因为语义可能并不总是可用的。 这些组合应该优于几乎所有其他证明的一类重要的问题。 技术能够有效的定理证明集的数百万输入条款也将寻求。

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.