Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden


Unification Modules for KEIM

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 You can fetch

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.

home Jörn Richts, last changed 25.06.1999.