Hyperproof is a system for learning the principles of analytical reasoning and proof construction, consisting of a text and a Macintosh software program. Unlike traditional treatments of first-order logic, Hyperproof combines graphical and sentential information, presenting a set of logical rules for integrating these different forms of information. This strategy allows students to focus on the information content of proofs rather than the syntactic structure of sentences. It also reflects the heterogeneity of information encountered in everyday reasoning.

Using Hyperproof the student learns to construct proofs of both consequence and non-consequence using an intuitive proof system that extends the standard set of sentential rules to incorporate information represented graphically. Proofs of consistency and inconsistency are also covered as well as independence proofs. The Hyperproof software checks the logical validity of each type of proof.

Hyperproof is compatible with various natural-deduction-style proof systems, including the system used in the authors' The Language of First-order Logic.

Hyperproof is designed to be used in a first course in logic. Since it presupposes familiarity with the program Tarski's World , it should be used in tandem with either the textbook The Language of First-order Logic or the stand-alone version of Tarski's World ( Tarski "Lite"). Hyperproof is currently available only for the Macintosh.

Jon Barwise and John Etchemendy have developed several other logic courseware packages. Information on these packages can be be found at http://ggweb.gradegrinder.net/openproof/.

Jon Barwise (1942–2000) was director of the Symbolic Systems Program and professor of philosophy at Stanford University and a researcher at CSLI.

John Etchemendy is professor of philosophy at Stanford University.

This book and software has been superceded by Logical Reasoning
with Diagrams & Sentences, Using Hyperproof

- 1 About Hyperproof
- How to use this book
- With LoFOL
- With
*Tarski Lite*

- Acknowledgements
- A note to instructors
- Hyperproof on the World-Wide Web

- I Basic Concepts
- 1 Comparing Tarski's World and Hyperproof
- 1.1 Worlds and situations
- 1.2 A new property and reltion
- 1.3 Language differences
- 1.4 Kleen Elevation
- 1.5 Proofs

- 2 Proofs of Consequence and Nonconsequence
- 2.1 Observe
- 2.2 Assume
- 2.3 Check Truth of the Assumptions (CTA)
- 2.4 Sentence goals

- 3 Sentential Consequence Rules
- 3.1 Tautological Consequence
- 3.2 Logical Consequence
- 3.3 Analytic Consequence

- 4 Proofs of Consistency and Inconsistency
- 4.1 Syntactic Close
- 4.2 Semantic Close
- 4.3 Consistency goals

- II Diagrammatic Reasoning
- 5 The Apply Rule
- 5.1 Apply
- 5.2 Some situations and goals

- 6 Reasoning by Cases
- 6.1 Cases Exhaustive
- 6.2 Merge and Inspect
- 6.3 Recursive Close
- 6.4 Name
- 6.5 Review exercises

- 7 Independence Proofs
- 7.1 Consequence, nonconsequence and independence
- 7.2 More independence goals
- 7.3 Constrained independence and consequence
- 7.4 Some final situation goals
- 7.5 Review exercises

- III Sentential Reasoning
- 8 Sentence Connective Rules
- 8.1 Conjunction rules
- 8.2 Disjunction rules
- 8.3 Negation Rules
- 8.4 Conditional rules
- 8.5 Biconditional rules
- 8.6 Matters of style

- 9 Quantifier and Identitiy Rules
- 9.1 Identiy Rule
- 9.2 Existential quantifier rules
- 9.3 Universal quantifier rules
- 9.4 Multiple quantifiers
- 9.5 Numerical quantifier rules
- 9.6 Reveiew Exercises

- 10 Axioms and Analytic Consequence
- 10.1 The axiomatic method
- 10.2 Axiomatizing Shape
- 10.3 Axiomatizing size
- 10.4 Locating Axioms

- 11 Logic and Observation

- A Using Hyperproof
- A.1 Launching the program
- A.2 Editing the situation
- A.3 The Body of the proof
- A.4 Goals
- A.5 Copying and pasting
- A.6 Printing proofs
- A.7 Function keys
- A.8 Setting up problems
- A.9 Projecting Hyperproof in class

- B Summary of Goals
- C The LoFOL Proof System
- Index
- Index of You Try It Files

1/1/94