Satallax内部指南
Internal Guidance for Satallax
摘要：
我们提出了一个新的内部指导方法的基础上的自动定理证明的给定子句算法。我们的方法影响选择未处理的条款，使用正面和负面的例子，从以前的证明。为此，我们提出了一个有效的方案，朴素贝叶斯分类一般化标签的出现与幺半群结构的类型。这使得有可能扩展现有的快速分类器，它只考虑正面的例子，与负面的。我们实现的方法在高阶逻辑证明Satallax，在那里我们修改的延迟与命题的处理。我们在Flyspeck项目的一个简单类型的高阶逻辑版本上评估了我们的方法，在没有内部指导的情况下，它比Satallax多解决了26%的问题。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
