Productive use of failure in inductive proof
Productive use of failure in inductive proof
复制标题
DOI：
10.1007/bf00244460
复制
发表时间：
1996-03-01
期刊：
影响因子：
--
通讯作者：
Bundy, A
中科院分区：
文献类型：
--
作者：
Ireland, A;Bundy, A
通过数学归纳法的证明产生了各种各样的尤里卡步骤，例如，缺少引理和推广。大多数归纳定理证明器依赖于用户干预提供所需的尤里卡步骤。相反，我们提出了一种新的定理证明架构，支持自动发现的尤里卡步骤。我们建立在涟漪，搜索控制启发式设计的归纳推理。我们展示了如何失败，如果涟漪可以用来弥合差距，在寻找归纳证明。
Proof by mathematical induction gives rise to various kinds of eureka steps, e.g., missing lemmata and generalization. Most inductive theorem provers rely upon user intervention in supplying the required eureka steps. In contrast, we present a novel theorem-proving architecture for supporting the automatic discovery of eureka steps. We build upon rippling, a search control heuristic designed for inductive reasoning. We show how the failure if rippling can be used in bridging gaps in the search for inductive proofs.