The Graphical User Interface of INKA

Dieter Hutter, Claus Sengler

In: Nicholas A. Merriam (Hrsg.). Proceedings International Workshop on User Interfaces for Theorem Provers. Workshop on User Interfaces for Theorem Provers (UITP-96) July 19 York United Kingdom Seiten 43-50 N. Merriam 1996.


The development of software components, that are provably correct with respect to a formal specification, requires semantic conditions to be formalized and proved. Only then, the corresponding development step is guaranteed to be correct. Besides the adequacy of the concepts underlying the overall development method, the time and skill necessary to fulfill these proof obligations are the main limiting factors for an application of formal techniques. Powerful deduction systems are therefore essential components of computer-aided software development systems. The INKA system is a first-order theorem prover with induction, and it is designed to be used for practical applications such as the formal development of software. Therefore, INKA possesses an interaction facility which follows the paradigm of direct manipulation. Any proof or proof attempt is summarized as a proof sketch which contains all deduction steps done so far as well as the strategic information concerning the way of proving the remaining tasks. It is presented to the user in a graphical representation on several abstraction layers. Both, the human user and the machine will alternatively edit this proof sketch until a complete proof is achieved. (gz, 56 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence