Automated Deduction—CADE-11
Automated Deduction—CADE-11
复制标题
自动推导—CADE-11
DOI：
10.1007/3-540-55602-8
复制
发表时间：
1992
影响因子：
1.3
通讯作者：
A. Bundy
中科院分区：
文献类型：
--
作者：
T. Walsh;A. Nunes;A. Bundy
我们描述了一个程序，用于寻找封闭形式的解决方案，以有限的总和。该程序是为了测试证明规划搜索控制技术在数学领域的适用性而建立的。这个实验是成功的。该系列求和程序扩展了以前在这方面的工作，并在很短的时间内建成，只是通过提供新的系列求和方法，我们现有的归纳定理证明系统CLAM。一个令人惊讶的发现是有用的therippletactic求和系列。波动是控制归纳证明的关键策略，以前被认为是专门用于这种证明的。然而，它被证明是所有用于求和序列的主要策略所使用的关键子策略。唯一需要的改变是，它必须由一个差异匹配算法来补充，以建立一些初始的元级注释来指导涟漪过程。在归纳证明中，这些注释是由数学归纳法的应用提供的。这一证据表明，涟漪，辅以差异匹配，将发现广泛的应用在控制数学证明。
We describe a program for finding closed form solutions to finite sums. The program was built to test the applicability of theproof planningsearch control technique in a domain of mathematics outwith induction. This experiment was successful. The series summing program extends previous work in this area and was built in a short time just by providing new series summing methods to our existing inductive theorem proving systemCLAM.One surprising discovery was the usefulness of therippletactic in summing series. Rippling is the key tactic for controlling inductive proofs, and was previously thought to be specialised to such proofs. However, it turns out to be the key sub-tactic used by all the main tactics for summing series. The only change required was that it had to be supplemented by adifference matchingalgorithm to set up some initial meta-level annotations to guide the rippling process. In inductive proofs these annotations are provided by the application of mathematical induction. This evidence suggests that rippling, supplemented by difference matching, will find wide application in controlling mathematical proofs.