next up previous contents index
Next: Evaluation Up: Components of the Previous: Definitions

Proof Editing

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.

  1. prove A
  2. prove B

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.

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