We propose a new internal guidance method for automated theorem provers based on the given-clause algorithm. Our method influences the choice of unprocessed clauses using positive and negative examples from previous proofs. To this end, we present an efficient scheme for Naive Bayesian classification by generalising label occurrences to types with monoid structure. This makes it possible to extend existing fast classifiers, which consider only positive examples, with negative ones. We implement the method in the higher-order logic prover Satallax, where we modify the delay with which propositions are processed. We evaluated our method on a simply-typed higher-order logic version of the Flyspeck project, where it solves 26% more problems than Satallax without internal guidance.

提出了一个基于给定句子算法的自动定理证明器的新的内部指导方法，该方法使用先前证明中的正负例影响未处理子句的选择。为此，提出了一种基于幺半群结构的类型广义标签出现次数的朴素贝叶斯分类的有效方案。将这种方法在高阶逻辑证明器Satallax中完成，证明了该方案比不具有内部指导的Satallax可以解决更多问题，能够扩展现有的快速分类器。在Flyspeck项目的一个简单类型的高阶逻辑版本上评估了我们的方法，在没有内部指导的Satallax不能解决的26%的问题上可以解决。

Satallax的内部指导