[IMAGE ]
Figure 1: A screen dump from Hyperproof. Blocks can have one of
three known shapes (tetrahedron, dodecahedron, or cube) and one of
three known sizes (small, medium, or large). Notations are provided
for leaving either or both of these attributes unspecified. Each
square on the grid is capable of holding at most one block. There are
spaces to the right of the grid that can be used for blocks whose
location is undetermined. Facilities also exist for specifying unary
and binary predicates on blocks.
Hyperproof is a heterogeneous logic; the term heterogeneous arises from the formal integration of the diagrammatic and sentential representations [3]. A sample screen appears in Figure 1. Hyperproof has several benefits from an instructional standpoint. First, the diagrams help students focus on the subject matter of the problem, forcing them to think about the problem rather than the syntactic form in which it happens to be stated.
Second, using the diagrams in working out proofs often greatly simplifies both the proofs and the process of discovering them. This reflects the fact that people often use visual information, including diagrams, in problem solving, and that they generally reason with information from a variety of representations simultaneously. The system therefore provides a more ``natural'' domain for reasoning which many students find more approachable than first-order logic alone.
Third, the system allows problems to be stated in a neutral problem solving format. Rather than simply ask a student to prove something, one can ask whether or not something follows from the information presented. The student is forced to think not just about how to prove the possible conclusion, but whether it in fact follows. If it does, the student presents a proof. If it does not, it is up the the student to present a proof that it does not. In either case, the proof makes crucial use of the diagrammatic aspect of the system.
Fourth, the inference rules of the system are designed to stress the main methods of valid reasoning, postponing intricacies of syntactically sophisticated rules until after these methods are mastered. These methods include:
Methods are also provided for checking that all the given information holds but that some purported conclusion fails in a diagram. Naturally, Hyperproof also contains the standard inference rules of first-order predicate logic.
Finally, the diagram assists students in determining which of the many known properties should be explored exhaustively. This is one advantage to Hyperproof over a semantic tableaux approach; although tableaux also support proof development by splitting into cases, they offer no guidance as to which cases are important. Such information can often be gleaned from the diagrams because there is often a hierarchical relationship between elements of the universe that reflects their impact on a proof. Locating that relationship is crucial to developing concise proofs. Consider for example the boolean expression
Splitting into cases on a immediately reduces this expression to false, while splitting on either b or c before splitting on a requires more steps to reduce the expression to false. It follows that a has a more crucial role in this proof. Notations that facilitate finding such hierarchical relationships are useful for developing concise proofs. Hierarchical relationships are often spatial in nature; diagrams are a natural representation for spatial information. Venn diagrams, for example, naturally represent hierarchy for set-relationship problems. More detailed examples of the role of hierarchical information in reasoning appear in [2].