The Inductive Theorem Prover INKA, Version 4.0

The INKAsystem 4.0 is a firstorder theorem prover with induction
which is based on the explicit induction paradigm. It is based
on a full firstorder calculus (a special variant of the
resolution calculus with paramodulation)
Main Features:

The system possesses a powerful predicatelogic prover
component which (as already mentioned) is based on an order
sorted variant of a resolution calculus with paramodulation.

A variety of definition principles are offered to define
data types (with free constructors as well as with nonfree
constructors), functions and predicates. For functions and
predicates additional definition principles are offered for
algorithmic specifications.

A builtin recursion analysis ensures the termination
of the above mentioned algorithms. The encoded wellfounded
order relation can then be used to formulate the induction
axioms.

Sophisticated heuristics based on the notions of
rippling and of colouring formulas are used to guide the
proof search by proof plans.

In either way, if the proof search succeeds or if the
proof search fails, the user is offered a (graphical)
representation of the proof attempt. The user can interact
with the system by giving the system some advice for filling
the gap in the proof sketch.

In order to make the use of the INKA system in practical
applications more comfortable, certain predefined data types
are at hand together with special builtin procedures for
their treatment. These predefined data types include finite
sets, finite arrays, and integers.
INKA User Interface:
The INKASystem 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 INKASystem 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
Download:
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.
Contact:
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
 D. Hutter, C. Sengler:
INKA, The Next Generation,
Proceedings of the 13th CADE, LNAI, Springer, 1996
 S. Biundo, B. Hummel, D. Hutter, C. Walther:
The Karlsruhe Induction Theorem Proving System,
Proceedings of the 8th CADE, LNCS 230, Springer, 1986
 D. Hutter: Complete Induction,
in: Deduction Systems in Artificial Intelligence,
Editor: K.H. Bläsius and H.J. Bürckert,
Ellis Horwood, 1989
 D. Hutter: Automatisierung der Vollständigen Induktion,
in: Deduktionssysteme,
Editor: K.H. Bläsius and H.J. Büurckert,
Oldenbourgh Verlag, 2. Auflage, 1992
 C. Walther: Mathematical Induction,
in: Encyclopedia of Artificial Intelligence
Editor: S.C. Shapiro, John Wiley and Sons, 1991
 C. Walther: Mechanizing Mathematical Induction,
in: Handbook of Logic in Artificial Intelligence
and Logic Programming,
Editor: B.M. Gabbay, C.J. Hogger and J.A. Robinson,
Oxford University Press, 1992
The Calculus
 C. Walther:
A ManySorted Calculus Based on Resolution and Paramodulation,
Research Notes in Artificial Intelligence, Pitmann Ltd, 1987
 D. Hutter:
Adapting a Resolution Calculus for Inductive Proofs,
Proceedings 10th European Conference on Artifical Intelligence,
Wiley and sons, 1992
Recursion Analysis and Induction Synthesis:
 C. Walther:
ArgumentBounded Algorithms as a Basis for
Automated Termination Proofs,
Proceedings 9th CADE, LNCS 310 Springer, 1988
 C. Walther: Automatisierung von Terminierungsbeweisen,
Vieweg Verlag, 1991
 D. Hutter:
Synthesis of Induction Orderings for Existence Proofs,
Proceedings 12th CADE, LNAI 814, Springer, 1994
 C. Walther: Computing Induction Axioms,
Proceedings of the LPAR92, 1992
 D. Hutter:
Using rippling to prove
the termination of algorithms.
Research Report RR 9703, DFKI GmbH, Saarbrücken, Germany, 1997.
User Interface:
Strategies:
 S. Biundo:
Automated Synthesis of Recursive Algorithms as a Theorem Proving Tool,
Proceedings 10th European Conference on Artifical Intelligence,
Wiley and sons, 1988
 D. Hutter: Guiding Induction Proofs,
Proceedings 10th CADE, LNCS 449, Springer, 1990
 D. Hutter:
Mustergesteuerte Strategien zum Beweisen von Gleichheiten ,
Ph.D. Thesis, Universitäat Karlsruhe, 1991
 D. Hutter:
Synthesis of Induction Orderings for Existence Proofs,
Proceedings 12th CADE, LNAI 814, Springer, 1994
 D. Hutter:
Colouring Terms to Control Equational Reasoning,
Journal of Automated Reasoning, 18:399442, 1997.
 D. Hutter:
Using Rippling for Equational Reasoning,
Proceedings KI96, Springer LNAI 1137, 1996