INduktionsbeweiser KArlsruhe is a semi-automated inductive theorem prover actively developed from 1985 till 1999. It is written in LISP (two versions: CMU-Lisp and Allegro-Lisp) and TCL/TK.
Main developers were: Serge Autexier, Susanne Biundo, Birgit Hummel, Dieter Hutter, Claus Sengler, and Christoph Walther