From honeydew.srv.cs.cmu.edu!das-news.harvard.edu!noc.near.net!howland.reston.ans.net!math.ohio-state.edu!cs.utexas.edu!uunet!math.fu-berlin.de!zib-berlin.de!news.dfn.de!coli.uni-sb.de!sbusol.rz.uni-sb.de!cs.uni-sb.de!nesmith Wed Sep 15 17:01:25 EDT 1993 Article: 11043 of comp.lang.lisp Xref: honeydew.srv.cs.cmu.edu comp.ai:18823 comp.ai.edu:1317 comp.lang.lisp:11043 comp.lang.clos:2034 Path: honeydew.srv.cs.cmu.edu!das-news.harvard.edu!noc.near.net!howland.reston.ans.net!math.ohio-state.edu!cs.utexas.edu!uunet!math.fu-berlin.de!zib-berlin.de!news.dfn.de!coli.uni-sb.de!sbusol.rz.uni-sb.de!cs.uni-sb.de!nesmith From: nesmith@cs.uni-sb.de (Daniel Nesmith) Newsgroups: comp.ai,comp.ai.edu,comp.lang.lisp,comp.lang.clos Subject: KEIM: CLOS Toolkit for Deduction Date: 15 Sep 1993 10:28:10 GMT Organization: Computer Science, University of the Saarland, Germany Lines: 58 Distribution: world Message-ID: <276qnqINNpk8@sbusol.rz.uni-sb.de> NNTP-Posting-Host: js-sfbslc10.cs.uni-sb.de Keywords: deduction, lisp, CLOS 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: keim@cs.uni-sb.de A mailing list for KEIM users is also being set up. Send mail to keim-users-request@cs.uni-sb.de to be put on the list.