Meta-level inference: Two applications

作     者：Bundy, Alan Sterling, Leon 

作者机构：Department of Artificial Intelligence University of Edinburgh United Kingdom 

出 版 物：《Journal of Automated Reasoning》 (J Autom Reasoning)

年 卷 期：1988年第4卷第1期

页      面：15-27页

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：algebra automatic programming IMPRESS learning meta-level inference PRESS proof plans search control theorem proving verification 

摘      要：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. © 1988 Kluwer Academic Publishers.