We investigate partial evalution of Prolog programs as a part of a theory of interactive, incremental programming. The goal of of this investigation is to provide formally correct, interactive programming tools for program transformation.

An abstract Prolog machine is introduced. The machine is systematically extended to an abstract partial evaluation Prolog machine. Three fundamental partial evaluation transformations are introduced and proved to preserve meaning of programs: pruning, forward data structure propagation, and opening (which also provides backward data structure propagation). The theoretical investigation is then extended to account for relations between logic and partial evalution.

An implementation of a partial evalution system is then developed from the formal specification. The system is well integrated and efficiently implemented in the Qlog programming environment. Several examples illustrate the mechanism and applications of partial evalution.

Finally, we outline how meta-rules that control the execution of the Prolog program can be incorporated into the system in a clean way. Such rules are familiar from artifical intelligence research. They could be used in future programming environments as specialized metatheories which support the programmer in particular tasks of programming.