Implicit induction in conditional theories
Implicit induction in conditional theories
复制标题
条件理论中的隐式归纳法
DOI：
10.1007/bf00881856
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
M. Rusinowitch
中科院分区：
文献类型：
--
作者：
A. Bouhoula;M. Rusinowitch
我们提出了一种新的条件理论中的归纳证明过程，其中案例分析是通过术语重写来模拟的。这种技术大大减少了应用归纳法时要考虑的猜想的变量数量。我们的过程被描述为一组推理规则，其正确性已经得到了形式化证明。此外，当公理是地面收敛的，并且函数被完全定义时，可以应用该系统来驳斥猜想。对于自由构造子上具有布尔前提条件的条件方程，该过程甚至是反驳完全的。该方法完全在proverSPIKE中实现。该系统以完全自动的方式解决了有趣的问题，也就是说，不需要与用户交互，也不需要特别的启发式算法。这也证明了具有挑战性的吉拉博尔特纸牌技巧，只有两个简单的lemma。
We propose a new procedure for proof by induction in conditional theories where case analysis is simulated by term rewriting. This technique reduces considerably the number of variables of a conjecture to be considered for applying induction schemes. Our procedure is presented as a set of inference rules whose correctness has been formally proved. Moreover, when the axioms are ground convergent and the functions are completely defined, it is possible to apply the system for refuting conjectures. The procedure is even refutationally complete for conditional equations with Boolean preconditions over free constructors. The method is entirely implemented in the proverSPIKE. This system has solved interesting problems in a completely automatic way, that is, without interaction with the user and without ad hoc heuristics. It has also proved the challenging Gilbreath card trick, with only two easy lemmas.