Proof Lab

ProofLab is one of the four central components of the AProS Project. It is a proof construction and student management system. The Lab offers a unique “backward-forward” proof representation through Fitch Diagrams. Students can apply rules backward in the Goal Tree, and forward in the Fitch Diagram. This representation allows students to employ in a very direct way the special strategies developed for the AProS Proof Engine.

The Proof Lab handles ‘bureaucratic work’ for students, allowing them to focus on the structure of arguments. On the one hand, it keeps track of justifications and applies rules in the Fitch Diagram, after they have been specified by the student. On the other hand, the Proof Lab points out mistakes, when students misapply a rule (for instance, applying elimination rule for the conditional to a conjunction) or mix separate subproofs. It provides the student with information to correct mistakes.

The Proof Lab is used as a workbench in the Logic & Proofs course. However, it is designed so that it can be offered, in the future, as a companion to other logic courses that include a treatment of natural deduction. Finally, the Proof Lab saves partial and completed proofs for reference, but manages also information for students (grades, records of completed exercises etc.); it utilizes the OLI Grade-book to present these data.