The proof--editing facility supports top--down construction of proofs. Goals are written as sequents ; they have the form :,,: >> G, where the are the hypotheses and G is the conclusion. To prove a goal , the user selects a rule for making progress toward achieving this goal, and the system responds with a list of subgoals . For example, if the goal is prove A&B and the rule selected is ``and introduction,'' the system generates the following subgoals.
Proofs can be thought of as finite trees, where each node corresponds to the application of a logical rule. A proof can be read to the desired level of detail by descending into subtrees whose structure is interesting and passing over others.