The Inductive Theorem Prover INKA, Version 4.0
|
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:
-
The system possesses a powerful predicate-logic 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 non-free
constructors), functions and predicates. For functions and
predicates additional definition principles are offered for
algorithmic specifications.
-
A built-in recursion analysis ensures the termination
of the above mentioned algorithms. The encoded well-founded
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 built-in procedures for
their treatment. These predefined data types include finite
sets, finite arrays, and integers.
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
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 Many-Sorted 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:
Argument-Bounded 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 LPAR-92, 1992
- D. Hutter:
Using rippling to prove
the termination of algorithms.
Research Report RR 97-03, 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:399-442, 1997.
- D. Hutter:
Using Rippling for Equational Reasoning,
Proceedings KI-96, Springer LNAI 1137, 1996