CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

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.
See Also: 


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 Postfach 1150 D-66041 Saarbruecken, Germany Keywords: 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 References: ?
Last Web update on Mon Feb 13 10:27:32 1995