The Use of Explicit Plans to Guide Inductive Proofs
The Use of Explicit Plans to Guide Inductive Proofs
复制标题
使用显式计划来指导归纳证明
DOI：
--
复制
发表时间：
1988
期刊：
影响因子：
--
通讯作者：
A. Bundy
中科院分区：
文献类型：
--
作者：
A. Bundy
我们建议使用明确的证明计划，以指导在自动定理中搜索证明证明。通过将证明计划表示为类似LCF的策略的规格，[Gordon等79]，并将这些规格记录在排序的元逻辑中，我们能够推荐证明的猜想以及可证明它们的方法。通过这种方式，我们可以构建广泛普遍性的证据计划，正式考虑并预测其成功和失败，灵活地应用它们，从失败中恢复过来，并从示例证明中学习它们。
We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and by recording these specifications in a sorted meta-logic, we are able to reason about the conjectures to be proved and the methods available to prove them. In this way we can build proof plans of wide generality, formally account for and predict their successes and failures, apply them flexibly, recover from their failures, and learn them from example proofs.