We have had great success teaching with Hyperproof in the classroom. Our experiences, student feedback, and feedback from other instructors indicate that several features of Hyperproof make it an extremely useful tool. The first is its use of visual displays of information.
Before teaching with Hyperproof, we had students learn logic by translating English sentences into sentences of first-order logic containing letters and symbols and then manipulating those symbols according to rules of logic. Unfortunately, the most common result of this approach was that students became excellent symbol manipulators, but had a hard time applying that skill to actual reasoning problems. This arose because students focused on the symbol manipulation, rather than on the problem and the logical concepts being taught. As a result, solutions to reasoning problems typically lost contact with the problem.
When students can see what they are reasoning about and when diagrams are an integral part of a proof as they are in Hyperproof, students achieve far greater understanding of the principles of reasoning than is otherwise possible. Evidence of this comes in numerous forms. For example, students repeatedly convey thoughts such as ``having the diagrams makes the reasoning easy to understand.'' In addition, we have found that we can cover the course content in a much shorter time using Hyperproof than we can teaching in more traditional ways, primarily because it is much easier for the students to learn the concepts.
Two other features that contribute to Hyperproof's success in the classroom is the fact students can check their proofs as they are doing them and that there is a grading program for instructors. Each line in a proof can be checked for validity and the entire proof can be checked to determine whether the given goal has been satisfied. When a step is invalid, in many circumstances a hint is given to indicate what the student is doing wrong. Students repeatedly report that they like the fact that they can identify and correct mistakes immediately, without having to wait until their homework is graded and returned to find out whether they are doing their work correctly. We have found that most of the time students turn in errorless proofs.
The great benefit of the grader is that the instructor can grade large numbers of proofs quickly. For example, in a class of forty students, we can assign a homework assignment consisting of ten proofs and grade all the proofs in an hour or two. Grading the same number of handwritten proofs would be too time-consuming; we would have to assign less proofs or simply not grade them all.