next up previous contents index
Next: Basics of the Up: System Description Previous: Copying and Moving

The Proof Editor

  proofs are sequent  proofs organized in a refinement style. In other words they are trees where each node contains a goal  and a rule  application. The children of a node are the subgoals  of their parent; in order to prove the parent it is sufficient to prove the children. ( automatically generates the children, given their parent and the rule to be applied; it is never necessary to type them in.) Not all goals have subgoals; for example, a goal proved by hyp does not. Also, an incomplete goal (one whose rule is bad or missing) has no subgoals.

In what follows the main goal ( the goal for short) is the goal of the current node; a goal is either the main goal or one of its subgoals.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995