Using meta-level inference for selective application of multiple rewrite rule sets in algebraic manipulation

摘要

In this paper we describe a technique for controlling inference, called meta-level inference, and a program for algebraic manipulation, PRESS, which embodies this technique. In PRESS, algebraic expressions are manipulated by a series of methods. The appropriate method is chosen by meta-level inference and itself uses meta-level reasoning to select and apply rewrite rules to the current expression.The use of meta-level inference is shown to drastically cut down on search, lead to clear and modular programs, aid the proving of properties of the program and enable the automatic learning of both new algebraic facts and new control information.