Automated Theorem Proving by Test Set Induction
Automated Theorem Proving by Test Set Induction
复制标题
通过测试集归纳自动证明定理
DOI：
10.1006/jsco.1996.0076
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
A. Bouhoula
中科院分区：
文献类型：
--
作者：
A. Bouhoula
测试集归纳是一种目标导向的证明技术，它结合了显式归纳和一致性证明的全部功能。它的工作原理是通过计算一个适当的显式归纳方案称为测试集，以触发归纳证明，然后应用反驳原则，使用一致性证明技术。我们提出了一个通用的测试集归纳方案，并给出了一个简单的可靠性证明。我们的方法是基于新的概念的测试集，归纳变量，和可证明的不一致性，这使我们能够反驳错误的假设，即使在的情况下，功能没有完全定义。我们展示了如何测试集可以计算时的构造函数是不自由的，并给出了一个算法计算感应变量。最后，我们提出了一个程序证明测试集归纳这是反驳完整的一个更大的类的规格比已经在以前的工作。该方法已在proverSPIKE中实现。基于计算机实验处理互感，SPIKE似乎是更实用和更有效的显式归纳为基础的系统。
Test set induction is a goal-directed proof technique which combines the full power of explicit induction and proof by consistency. It works by computing an appropriate explicit induction scheme calleda test set, to trigger the induction proof, and then applies a refutation principle using proof by consistency techniques. We present a general scheme for test set induction together with a simple soundness proof. Our method is based on new notions of test sets,induction variables, andprovable inconsistency, which allow us to refute false conjectures even in the case where the functions are not completely defined. We show how test sets can be computed when the constructors are not free, and give an algorithm for computing induction variables. Finally, we present a procedure for proof by test set induction which is refutationally complete for a larger class of specifications than has been shown in previous work. The method has been implemented in the proverSPIKE. Based on computer experiments dealing with mutual induction,SPIKEappears to be more practical and efficient than explicit induction based systems.