InKa

InKa - an inductive theorem prover. InKa: 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.