Proof Tutor

The Proof Tutor Project was begun more than a decade ago with what seemed to be a very direct and straightforward idea; namely,

• teach logical argumentation within a computer-based course;
• have students give natural deduction proofs in an interface that allows working backward and forward;
• use an automated dynamic tutor to help students find proofs.

For the last item one should exploit a theorem prover that searches for natural deduction proofs in a strategically motivated way. This basic idea was articulated in 1986/87. Now we are finally at a stage where this vision can be realized.

We have developed the web-based course Logic & Proofs that provides a thorough introduction to classical sentential and predicate logic with a sharp focus on proof construction. Students can give proofs in the Proof Lab, a sophisticated interface that allows working backward and forward in an attempt to construct an argument. Finally, we also developed the appropriate logical meta-theory providing the basis for automated natural deduction proof search and an implementation of efficient strategies in AProS. These strategies are centrally taught in Logic & Proofs. What is missing from the basic idea? Its petutorogical centerpiece, the Proof Tutor. That is to be a dynamic, but gentle tutor, which interacts with students "intelligently" as follows. Students are trying to solve a proof construction problem in the lab and come to a point where no path to a solution is visible for them. An appeal to the proof tutor yields at first broad strategic advice that is based on the structure of the proof, efficiently found by AProS. That broad advice is, on further appeal, successively refined to a recommendation of the very next step that should be taken in the proof.