(which indicates
that an automatic proof has been attempted but failed). If we select Execute Task, an interactive proof
with the following root situation is created:
The previous sections dealt mainly with tasks (type-checking conditions) that could be automatically solved by the integrated decision procedure. In this section, we discuss in somewhat more detail what happens if the automatic decision procedure does not succeed, in particular because it is impossible to achieve the goal of the task (i.e. the task is a priori doomed to fail).
One kind of failure (the goal of a proof is contradictory) can be demonstrated by the theory
which attempts to erroneously define an empty type T (by an interval of the integers whose lower bound is bigger than the upper bound). Type-checking this theory generates the task
The task is labeled in red (which indicates task status “open”) with the icon (which indicates
that an automatic proof has been attempted but failed). If we select Execute Task, an interactive proof
with the following root situation is created:
This situation depicts as knowledge three formulas derived from the base theory and no goal formula. The reason for the disappearance of the goal can be inferred by pressing the button “View Declarations” which depicts (among others)
From this, the goal a ≤ b was automatically reduced to FALSE and consequently discarded from the
proof situation. The proof could be thus only completed if the knowledge were inconsistent (such that
FALSE could be derived) which is here not the case. We therefore press the button Quit Proof 
and return (after a confirmation) to the “Analysis” view with task status still unchanged as indicated
by the icon .
Another kind of failure (the goal of a proof is unprovable) can be demonstrated by the theory
which defines a type as a subrange of the integers with unspecified bounds a and b. Type checking this theory yields the task
Also for this task the automatic proof fails and it is consequently indicated by the red label as “open”. If we select Execute Task, an interactive proof with the following root situation is created:
The knowledge is consistent but does not say anything about the variables a and b referred in the goal. By pressing the button View Declarations, the declarations related to the proof are shown below:
Since a and b have no defined values, there is no chance of completing the proof successfully. We
therefore press again the button Quit Proof and return to the “Analysis” view.
It may also (infrequently) happen that the type-checker generates tasks that cannot be solved by the integrated automatic decision procedure but can be solved by an interactive proof. If this should be the case, the proof remains persistent across multiple invocations of the RISC ProgramExplorer; it can be later displayed (menu option Print Status Evidence) and also replayed again (menu option Execute Task). Menu option Reset Task erases the proof and returns the task to state “new”.
If there is no ongoing interactive proof, the user may also manually switch to the “Verification” view and enter declarations and commands of the RISC ProofNavigator. The use of the software is then essentially the same as in the standalone version of the RISC ProofNavigator.
Thus the RISC ProofNavigator is already fully integrated into the task solution framework of the RISC ProgramExplorer; while this is not of major importance for the purpose of verifying type checking conditions, it becomes essential for verifying program correctness as discussed in the following chapter.