> and there's a much fancier one in LISP that's part of the LKB:
>
> http://wiki.delph-in.net/moin/LkbTop
related to the LKB implementation, a good overview of the history of graph unification algorithms is provided in Ulrich Callmeier's (2001) MSc thesis:
http://www.coli.uni-sb.de/~uc/thesis/thesis.pdf
his open-source PET system implements several unifiers in C[++], see:
http://wiki.delph-in.net/moin/PetTop
http://pet.opendfki.de/browser/pet/main/cheap/dag-tomabechi.cpp
note, however, that neither the LKB nor PET provide some of the extra devices you mention, e.g. TFS disjunction or negation and sets. with moving more linguistic contraints into the type system, these seem to have gone somewhat out of fashion since the mid-1990s.
all best - oe
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ +++ Universitetet i Oslo (IFI); Boks 1080 Blindern; 0316 Oslo; (+47) 2284 0125 +++ CSLI Stanford; Ventura Hall; Stanford, CA 94305; (+1 650) 723 0515 +++ --- oe at ifi.uio.no; oe at csli.stanford.edu; stephan at oepen.net --- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++