Higher-Order Annotated Terms for Proof Search
Higher-Order Annotated Terms for Proof Search
复制标题
用于证明搜索的高阶注释术语
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
I. Green
中科院分区：
文献类型：
--
作者：
A. Smaill;I. Green
嵌入适当的高阶语法的概念进行了描述。这提供了根据公式对之间的差异的注释公式的表示。我们为这些注释术语定义了替换和统一。使用注释术语的这种表示，涟漪的证明搜索指导技术可以扩展到高阶定理。我们用两个选择的例子来说明这一点，使用我们在λProlog中实现这些想法。
A notion of embedding appropriate to higher-order syntax is described. This provides a representation of annotated formulae in terms of the difference between pairs of formulae. We define substitution and unification for such annotated terms. Using this representation of annotated terms, the proof search guidance technique of rippling can be extended to higher-order theorems. We illustrate this with two selected examples using our implementation of these ideas in λProlog.