We give the first Goal-Directed version 
of the Knuth Bendix Completion Procedure.  
Our procedure is based on Basic Completion 
and SOUR Graphs.  There are two phases to 
the procedure.  The first phase, which runs 
in polynomial time,  compiles the equations 
and the goal into a constrained tree automata 
representing the completed system, and a set 
of constraints representing goal solutions.  
The second phase starts with the goal solutions
and works its way back to the original 
equations, solving constraints along the way.