The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge


Research Paper #164

Title:CONTROLLING INFERENCE IN A SEMANTICALLY RICH DOMAIN
Authors:Bundy, A; Sterling, L
Date:Sep 1981
Presented:Submitted to the Workshop on Logic Programming for Intelligent Systems, Los Angeles.,16th September 1981
Keywords:
Abstract:We describe two uses of meta-level inference: to control the search for aproof, 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.
Download:PDF COPY


[Search These Pages] [DAI Home Page] [Comment]