The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling
The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling
复制标题
使用嵌入为高阶波纹提供术语和注释的清晰分离
DOI：
10.1007/s10817-010-9177-y
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Dennis L
中科院分区：
文献类型：
--
作者：
Dennis L
涟漪是一种特殊应用于数学归纳法证明的证明搜索引导技术。它基于注释两个术语之间差异的概念。在最初的公式中，这个注释只适用于一阶公式。我们使用嵌入的概念来适当地调整这些注释以适应高阶语法。这种表示简化了注释项的理论，不再需要特殊的替换和统一定理。这种表示的一个关键特性是，它提供了术语和注释的清晰分离。我们通过在λ clam中实现这些想法的示例来说明这一点。
Ripplingis a proof search guidance technique with particular application to proof by mathematical induction. It is based on a concept of annotating the differences between two terms. In its original formulation this annotation was only appropriate to first-order formulae. We use a notion ofembeddingto adapt these annotations appropriately for higher-order syntax. This representation simplifies the theory of annotated terms, no longer requiring special substitution and unification theorems. A key feature of the representation is that it provides a clean separation of the term and the annotation. We illustrate this with selected examples using our implementation of these ideas inλClam.
登录
查看更多内容
DOI：
--
发表时间：
2001
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
作者：
Shuochao Yao;Shaohan Hu;Shen Li;Yiran Zhao;Lu Su;Lance M. Kaplan;A. Yener;T. Abdelzaher
通讯作者：
T. Abdelzaher
用于证明搜索的高阶注释术语
DOI：
--
发表时间：
1996
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
作者：
A. Smaill;I. Green
通讯作者：
I. Green
系统描述：使用 Lambda-Clam 在高阶逻辑中进行证明规划
DOI：
--
发表时间：
1998
期刊：
CADE
影响因子：
--
作者：
J. Richardson;A. Smaill;I. Green
通讯作者：
I. Green
Rippling - 数学推理的元级指导
DOI：
10.1017/cbo9780511543326
发表时间：
2005
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
A. Bundy;D. Basin;D. Hutter;Andrew Ireland
通讯作者：
Andrew Ireland
DOI：
10.1007/bf00244460
发表时间：
1996-03-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Ireland, A;Bundy, A
通讯作者：
Bundy, A