ANNOUNCING
KEIM version 1.0
KEIM is a collection of software modules, written in Common Lisp with
CLOS, designed to be used in the production of theorem proving systems.
KEIM is intended to be used by those who want to build or use deduction
systems (such as resolution theorem provers) without having to write the
entire framework. KEIM is also suitable for embedding a reasoning component
into another Common Lisp program.
KEIM offers a range of datatypes implementing a logical language of type
theory (higher order logic), in which first order logic can be embedded.
KEIM's datatypes and algorithms include: types; terms (symbols, applications,
abstractions), environments (e.g., associating symbols with types);
unification and substitutions; proofs, including resolution and natural
deduction style.
KEIM also provides functionality for the pretty-printing, error
handling, formula parsing and user interface facilities which form a large
part of any theorem prover. Implementing with KEIM thus allows
the programmer to avoid a great deal of drudgery.
The KEIM architecture, based on CLOS (Common Lisp Object System), allows
great flexibility in the integration of new classes of objects. The
generic function paradigm allows one to specialize the behavior of a
function on a new type of object without changing its behavior on existing
objects and without having to rewrite existing code.
KEIM has been tested in Allegro CL 4.1 and Lucid CL 4.0 on Sun 4
workstations.
The KEIM Project is located in the Department of Computer Science
at the Universitaet des Saarlandes and is under the direction of Prof.
Joerg Siekmann. KEIM serves as the basis for the Omega-MKRP proof
development environment (successor to the MKRP project) and other theorem
provers in the German Deduction Effort, sponsored by the Deutsche
Forschungsgemeinschaft as "Schwerpunkt Deduktion."
KEIM is available for noncommercial use via anonymous FTP on the following
machines:
(Europe) js-sfbsun.cs.uni-sb.de:pub/keim/keim*
(N. America) ftp.cs.cmu.edu:/afs/cs/project/tps/keim/keim*
(For the last, you must cd to the directory /afs/cs/project/tps/keim in one
command because of AFS protections on intermediate directories).
For more information contact Dan Nesmith at the address below:
Fachbereich Informatik/AG Siekmann
Universitaet des Saarlandes
Postfach 1150
D-66041 Saarbruecken
Germany
Internet: ····@cs.uni-sb.de
A mailing list for KEIM users is also being set up. Send mail to
··················@cs.uni-sb.de to be put on the list.