We today released a new courseware package called Logical Reasoning with Diagrams and Sentences. The course teaches how to reason formally using first-order logic and our blocks world diagrams. The principles are applicable to other kinds of diagrammatic representations too. The software accompanying the package, Hyperproof, implements a formal heterogeneous proof system, which has inference rules which involve both the sentential and diagrammatic representation.
This package was previously published under the title Hyperproof in 1994. This new package is a complete rewrite of the software (the original ran only on Mac OS 8.x and 9.x) and includes access to the Grade Grinder Internet-based grading service.
The new package is the work of many, many people. Most notably Mike Murray who has done sterling work implementing the software. Many others who contributed code and performed QA on the application.
The package can be obtained from our store.