TY - JOUR
T1 - Meta-Level Inference: Two Applications
AU - Bundy, Alan
AU - Sterling, L.
PY - 1988
Y1 - 1988
N2 - 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.
AB - 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.
KW - PRESS
KW - IMPRESS
KW - meta-level inference
KW - proof plans
KW - search control
KW - theorem proving
KW - algebra
KW - verification
KW - automatic programming
KW - learning
U2 - 10.1007/BF00244511
DO - 10.1007/BF00244511
M3 - Article
VL - 4
SP - 15
EP - 27
JO - Journal of Automated Reasoning
T2 - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
SN - 0168-7433
IS - 1
ER -