Meta-level inference: Two applications
Meta-level inference: Two applications
复制标题
元级推理：两种应用
DOI：
10.1007/bf00244511
复制
发表时间：
1988
期刊：
影响因子：
--
通讯作者：
L. Sterling
中科院分区：
文献类型：
--
作者：
A. Bundy;L. Sterling
我们描述了两种使用元级推理：控制搜索的证明，并获得新的控制信息，并说明它们在域的代数方程求解。控制信息的推导是本文的重点。它涉及代数元理论中定理的证明。这些证明是由元元级推理指导的。我们正在开发一种元元语言来描述公式和证明计划，并建立了一个程序，IMPRESS，它使用这些计划来建立证明。我们详细描述了一个这样的证明计划。IMPRESS将成为一个自我改进的代数系统的一部分。
We describe two uses of meta-level inference: to control the search for a proof; and to derive new control information, and illustrate them in the domain of algebraic equation solving. The derivation of control information is the main focus of the paper. It involves the proving of theorems in the Meta-Theory of Algebra. These proofs are guided by meta-meta-level inference. We are developing a meta-meta-language to describe formulae, and proof plans, and have built a program, IMPRESS, which uses these plans to build a proof. We describe one such proof plan in detail. IMPRESS will form part of a self-improving algebra system.