CMU Artificial Intelligence Repository
KEIM: Tools for Building Theorem Provers
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.
Version: 1.1 (10-OCT-93)
Requires: Common Lisp, CLOS
Ports: KEIM has been tested in Allegro CL 4.1 and Lucid CL 4.0
on Sun4 workstations.
Copying: Copyright (C) 1993 by AG Siekmann, Fachbereich Informatik,
Universitaet des Saarlandes, Saarbruecken, Germany.
Use, copying, modification, and distribution permitted
for noncommercial and non-safety-critical purposes only.
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Mailing List: To be added to the list, send mail to
Author(s): Dan Nesmith, Joerg Siekmann
Contact: Dan Nesmith
Fachbereich Informatik/AG Siekmann
Universitaet des Saarlandes
D-66041 Saarbruecken, Germany
Authors!Nesmith, Authors!Siekmann, Automated Reasoning,
CLOS!Code, Deduction Systems, First Order Logic, KEIM,
Lisp!Code, Natural Deduction, Reasoning!Automated Reasoning,
Resolution Theorem Proving, Substitutions, Theorem Proving,
Type Theory, Unification
Last Web update on Mon Feb 13 10:27:32 1995