Publikation
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, Pages 43-50, N. Merriam, 1996.
Zusammenfassung
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.