Edinburgh Research Explorer

Meta-Level Inference: Two Applications

Research output: Contribution to journalArticlepeer-review

Original languageEnglish
Pages (from-to)15-27
JournalJournal of Automated Reasoning
Issue number1
Publication statusPublished - 1988


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.

    Research areas

  • PRESS, IMPRESS, meta-level inference, proof plans, search control, theorem proving, algebra, verification, automatic programming, learning

ID: 401040