

automated proof search 

Proof LabProofLab is one of the five central components of the AProS Project. It is a proof construction and student management system. The Lab offers a unique “backwardforward” proof representation through Fitch Diagrams. This representation allows students to employ in a very direct way the special strategies developed for AProS. 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 Gradebook to present these data. 