ENIGMAWatch：ProofWatch与ENIGMA相遇
ENIGMAWatch: ProofWatch Meets ENIGMA
摘要：
在这项工作中，我们描述了一个新的基于学习的证明指导- ENIGMAWatch -饱和式一阶定理证明。ENIGMAWatch结合了两种用于E ATP系统的给定子句选择的指导方法：ProofWatch和ENIGMA。ProofWatch的动机是监视列表（提示）方法，基于多个相关证明的符号匹配，而ENIGMA基于统计机器学习。这两种方法相结合，通过使用符号证明匹配的演变信息作为一个额外的信息，表征饱和式证明搜索的统计学习方法。新系统的实验评估的一个大的问题集从Mizar图书馆。我们表明，增加的证明匹配信息被认为是重要的统计机器学习器，它导致改进E的性能超过ProofWatch和ENIGMA。
英文摘要：
In this work we describe a new learning-based proof guidance -- ENIGMAWatch -- for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the given-clause selection implemented for the E ATP system: ProofWatch and ENIGMA. ProofWatch is motivated by the watchlist (hints) method and based on symbolic matching of multiple related proofs, while ENIGMA is based on statistical machine learning. The two methods are combined by using the evolving information about symbolic proof matching as an additional information that characterizes the saturation-style proof search for the statistical learning methods. The new system is experimentally evaluated on a large set of problems from the Mizar Library. We show that the added proof-matching information is considered important by the statistical machine learners, and that it leads to improvements in E's Performance over ProofWatch and ENIGMA.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
