cl-unification
CL-Unification is a full blown unification library, supporting unification over any Common Lisp objects (and not just lists and atoms).

Homepage: http://common-lisp.net/project/cl-unification/

License: BSD

Pattern matching algorithm