Task Analysis

In the context of computer user interface design, a task is ``a structured set of activities in which actions are undertaken in some sequence'' [46], in order to achieve the user's goals. We define the user's goal to be formally proving some theorem, by some method of constructive proof.

A constructive proof can be though of as a tree of statements. At the root node is the subject of the proof: a statement of the theorem. Leaf nodes contain either axioms, or previously proven theorems. Internal nodes (nodes that aren't leaf nodes) are the result of applying inference rules to axioms and theorems, and are theorems themselves. The conjunction of child nodes implies the parent node.

These proof trees can be built either bottom-up, top-down, or some combination of the two. Trees built from the bottom up are known as forwards proof, and those built top-down are known as backwards proof.

Backwards proof works as follows:

• An initial goal (the theorem to be proven) is specified.
• Proof steps are applied repeatedly, transforming the existing goals into a set of sub-goals.
• The effect of proof steps may be reversed
• When all goals have been reduced to axioms or previously proven theorems, then the proof is complete.

Figure 3.1 shows a slightly more detailed view of how this is sometimes implemented.

Figure 3.1: Backwards proof