The Inductive Theorem Prover INKA, Version 4.0

Visit also the description of the new INKA 5.0 system

The INKA-system 4.0 is a first-order theorem prover with induction which is based on the explicit induction paradigm. It is based on a full first-order calculus (a special variant of the resolution calculus with paramodulation)

Main Features:

INKA User Interface:

The INKA-System has a sophisticated user interface based on the paradigm of direct manipulations. In order to get an impression of the interface click here

System Requirements:

The INKA-System currently runs under ALLEGRO COMMON LISP. Notice that Allegro Lisp can be obtained free of charge from Franz Inc. for Linux PC's.

You also need TCL/TK with versions greater or equal 8.0


To download INKA 4.0 click here .

You may also download a manual for INKA. I'm afraid that it is in German. Perhaps there is a volunteer to translate it in english.


In case of any problems feel free to contact me: Dieter Hutter

Selected Publications

These publications describe the rationals behind the development of INKA 4.0 until 1996/97. For more recent literature you may want to contact the general publication page of our group.

General Overview

The Calculus

Recursion Analysis and Induction Synthesis:

User Interface: