KEIM: A Toolkit for Automated Deduction

Xiaorong HuangXiaorong Huang, Manfred KerberManfred Kerber, Michael KohlhaseMichael Kohlhase, Erica MelisErica Melis, Dan NesmithDan Nesmith, Jörn RichtsJörn Richts, Jörg SiekmannJörg Siekmann

Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg Siekmann
KEIM: A Toolkit for Automated Deduction
In Alan Bundy, eds., Automated Deduction — CADE-12, Proceedings of the 12th International Conference on Automated Deduction, 807-810, 1994. Springer

Details
Bibtex

KurzfassungAbstract
KEIM is a collection of software modules, written in Common Lisp with CLOS, designed to be used in the implementation of automated reasoning 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. It offers a range of datatypes implementing a logical language of type theory (higher order logic), in which first order logic can be easily embedded. KEIM's datatypes and algorithms include: types; terms (symbols, applications, abstractions); unification and substitutions; proofs, including resolution and natural deduction styles.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ HuangKerber+-CADE-94,
  address = {Nancy},
  author = {Xiaorong {Huang} and Manfred {Kerber} and Michael {Kohlhase} and Erica {Melis} and Dan {Nesmith} and J{\"o}rn {Richts} and J{\"o}rg {Siekmann}},
  booktitle = {Automated Deduction --- CADE-12},
  editor = {Alan {Bundy}},
  pages = {807--810},
  publisher = {Springer-Verlag LNAI 814},
  series = {Proceedings of the 12th International Conference on Automated Deduction},
  title = {{KEIM}: A Toolkit for Automated Deduction},
  year = {1994},
}