UniMoK
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
- a Common Lisp including CLOS,
- KEIM 1.2.1 (was available from the OMEGA Project at AG Siekmann, Universität Saarbrücken, now available on GitHub).
You can fetch
- the whole UniMok system (600 kB),
- the unimok.README file with installation instructions,
- the copyright notice, or
- the complete KEIM and UniMoK system (9.4 MB).
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 the reseach project Combination of special deduction procedures funded by the Schwerpunkt "Deduktion" of the Deutsche Forschungsgemeinschaft.