Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts
Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts
复制标题
从多次证明尝试中自动获取搜索控制知识
DOI：
10.1006/inco.1999.2857
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
S. Schulz
中科院分区：
文献类型：
--
作者：
J. Denzinger;S. Schulz
我们提出了两种用于等式推导的推理控制启发法，它们基于对感兴趣领域中先前成功证明尝试的评估。第一个评估函数通过从知识库中符号检索广义模式来工作，第二个函数将知识编译成抽象术语评估树。这两种启发式方法都已被应用到分布式等式证明系统 DISCOUNT 中。我们分析了启发式方法在几组示例（包括 TPTP 集合中所有单位相等问题的子集）上的性能，并证明了它们的有用性。
We present two inference control heuristics for equational deduction that are based on the evaluation of previous successful proof attempts in domains of interest. The first evaluation function works by symbolic retrieval of generalized patterns from a knowledge base, and the second function compiles the knowledge into abstract term evaluation trees. Both heuristics have been implemented into the distributed equational proof system DISCOUNT. We analyze the performance of the heuristics on several sets of examples (including the subset of all unit-equality problems from the TPTP collection) and demonstrate their usefulness.