Thanks, Mark. I'll dig into it. Perhaps there will be something about unification. I've never heard of that term before.
I'll attempt a definition: Unification is the process of mapping two forms (e.g., equations) onto one another such that variables (in the form) are set to appropriate values and constraints are maintained. The process may involve backtracking, and can also end in failure (if no match is possible).
I did some web-hunting and this page seems like a reasonable intro to unification:
http://www.ccs.neu.edu/home/arthur/unif.html
I first learned about it reading Patrick Winston's first book on Lisp -- I remember typing in the code and poking at it forever trying to figure out how it was working. I think that the best description of the algorithm, though, is in Brian Harvey's "Computer Science Logo Style" series (Volume 3, I think). (In general, next to "Structure and Interpretation of Computer Programs," Harvey's books are my favorite CS texts.)
Mark
-------------------------- Mark Guzdial : Georgia Tech : College of Computing : Atlanta, GA 30332-0280 Associate Professor - Learning Sciences & Technologies. Collaborative Software Lab - http://coweb.cc.gatech.edu/csl/ (404) 894-5618 : Fax (404) 894-0673 : guzdial@cc.gatech.edu http://www.cc.gatech.edu/gvu/people/Faculty/Mark.Guzdial.html