Unification followed by unfolding. The left-hand side of

a rule is unified with some term, resulting in a set of

variable bindings. The term is then replaced by the

right-hand side of the rule with values substituted for boundvariables.