System Description: Proof Planning in Higher-Order Logic with Lambda-Clam
System Description: Proof Planning in Higher-Order Logic with Lambda-Clam
复制标题
系统描述：使用 Lambda-Clam 在高阶逻辑中进行证明规划
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
I. Green
中科院分区：
文献类型：
--
作者：
J. Richardson;A. Smaill;I. Green
这个系统描述概述了用于高阶逻辑中的证明规划的λClam系统。高阶证明规划的有用性和可行性，适用于一些类型的问题，特别是软件和硬件系统的合成和验证。高阶元理论的使用克服了Clam中遇到的问题，因为它无法正确地推理高阶对象。λClam是用λProlog编写的。
This system description outlines the λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying higher-order proof planning to a number of types of problem is outlined, in particular the synthesis and verification of software and hardware systems. The use of a higher-order metatheory overcomes problems encountered in Clam because of its inability to reason properly about higher-order objects. λClam is written in λProlog.