Proof Plans for the Correction of False Conjectures
Proof Plans for the Correction of False Conjectures
复制标题
纠正错误猜想的证明计划
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
Andrew Ireland
中科院分区：
文献类型：
--
作者：
R. Monroy;A. Bundy;Andrew Ireland
定理证明是通过使用推理规则从一组公理系统地推导出数学证明。我们感兴趣的是一个相关的，但很少探索的问题：错误命题的分析和纠正，特别是当纠正涉及到找到一组前因，连同一组公理，将非定理转化为定理。大多数失败的搜索树是巨大的，要特别小心，以解决组合爆炸现象。幸运的是，由证明计划生成的计划搜索空间，参见[1]，是适度小的。我们已经探讨了使用这种技术的可能性，在实施的溯因机制，以纠正非定理。
Theorem proving is the systematic derivation of a mathematical proof from a set of axioms by the use of rules of inference. We are interested in a related but far less explored problem: the analysis and correction of false conjectures, especially where that correction involves finding a collection of antecedents that, together with a set of axioms, transform non-theorems into theorems. Most failed search trees are huge, and special care is to be taken in order to tackle the combinatorial explosion phenomenon. Fortunately, the planning search space generated by proof plans, see [1], are moderately small. We have explored the possibility of using this technique in the implementation of an abduction mechanism to correct non-theorems.