Meta-level inference in Algebra

Alan Bundy, L. Sterling

Research output: Working paper


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. IMPRESS will form part of a self improving algebra system.
Original languageEnglish
Publication statusUnpublished - 1981

Publication series

NameDAI Research Paper 164


Dive into the research topics of 'Meta-level inference in Algebra'. Together they form a unique fingerprint.

Cite this