This installment of the notes describes a general lifting transformation that can be applied to arbitrary functional programs. Lifting was first introduced by Alan Robinson. It is the primary innovation of the original resolution procedure. Lifting is a relationship between two computational processes --- a "ground" computation and a "lifted" computation. The lifted computation is symbolic --- it involves variables and constraints. The lifted computation must "cover" the ground computation in the sense that the ground computation can be viewed as a substitution instance of the lifted computation.
These notes attempt to convey the intuition that any algorithm which manipulates ground expressions can be mechanically lifted. Once the general lifting transformation is understood there is no reason to present anything other than ground version of any algorithm. For example, lifting can be mechanically applied to the nonlinear planning procedures given in the previous intallment of the notes . Another example where mechanical lifting greatly improves clarity is the backward chaining locality algorithm given in the paper "New Results on Local Inference Relations". The ground algorithm presented there is sufficiently complex that an explicit formulation of the lifted version would be very difficult.
David McAllester, February, 1995