
Chapter
16:
Equivalences
of
Logic Programs
633
unifier of A and H such that
G
i+l
is ground. If the initial goal is ground, then
it is equivalent to say that a ground derivation is a derivation using the ground
instances of clauses of P. An SLD tree for a goal G is a tree with goals as
nodes where G is at the root, each non-empty goal contains a selected atom,
and the children of a node are the goals obtained in one derivation step using
the selected atom of that node.
The operational model we will use is fair SLD-resolution (Lassez and
Maher [1984]); that is, SLD-resolution where every branch of the SLD tree
forms a fair derivation. We conside ...