|
|
INKA - User Interface |
A detailed description of the INKA user interface can also be found in
From a theorem proving point of view, the user is mainly engaged in two activities: building up a specification and proving theorems with respect to this axiomatisation. At each stage of the proof synthesis, the human user can revise the proof sketch specified so far or give advice how to fill in the gaps. On the one hand the user should be able to construct any possible proof within the given calculus and for example even enforce the application of a single deduction step. On the other hand proofs should be found almost automatically and thus, the human interaction necessary to find a proof should be restricted to some strategic advice. Thus, INKA incorporate (human-like) strategic knowledge about proof search in order to facilitate users' hints. Conversely, the intentions of the (machine-like) built-in strategies have to be known by the user in order to efficiently assist the machine in the search for a proof. The essential means by which this contradictory mix of demands of the system are realized in INKA is the notion of a proof sketch. The representation of a proof sketch allows the user to edit them in several ways: he may give more precise hints for a proof sketch, which includes directives to apply a certain rule as the next step if the system gets stuck, or to revise hints, e.g.~by advising the system to use so-called bridge lemmata. He may add or delete subgoals, which includes the use of lemmata within proofs, and the possibility to correct the system's assumptions on intermediate steps. Finally, in extreme cases he may even replace the whole sketch including subgoals and hints.
