UniMoK is a system that contains unification algorithms for the free theory, for A, AC, and ACI. Furthermore it includes constraint solvers for rational trees and feature structures. The central part of UniMoK is a combination algorithm which allows two combine the component algorithms listed above.
The current implementation does not compute complete sets of unifiers but only provides decision procedures.
The current UniMoK version is 1.19. An update to 1.20 will follow soon.UniMoK needs
UniMok has been successfully installed and tested on Lucid Common Lisp V4.2 (Sun Sparc 10, Solaris 2.3) and Allegro Common Lisp V5.0 (Linux PC, Suse Linux 6.1). Allegro CL for PCs is freely available at Franz Inc..If you have any problems, send mail to Jan Hladik.
UniMoK was developed in a reseach
project funded by the Schwerpunkt
"Deduktion" of the Deutsche Forschungsgemeinschaft.