Overview   AProS   L & P   Proof Lab   Tutor   Truth Lab   Participants

automated proof search


Basic connections

The AProS Project was begun more than two decades ago under a different name, the Carnegie Mellon Proof Tutor Project. The Proof Tutor Project pursued 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. However, we thought then that it would be just a matter of asking colleagues in computer science to find a natural deduction theorem prover, re-writing Patrick Suppes' computer-based VALID course, programming a graphically appealing interface and designing a dynamic tutor. All these expectations were not quite right, and we are only now at a stage where this idea has been realized for full predicate logic.

The most extensive and central tasks were i) the development of an appropriate logical theory that provides the basis for natural deduction proof search and ii) the implementation of a search algorithm with efficient and natural strategies through AProS. We have developed a web-based course, Logic & Proofs, which provides a thorough introduction to classical sentential and predicate logic with a sharp focus on strategic proof construction. The natural strategies AProS uses are centrally taught in Logic & Proofs. Students can give proofs in the Proof Lab, a sophisticated interface that allows working backward and forward in an attempt to construct an argument.

Its pedagogical centerpiece, the Proof Tutor, has been implemented and is now being used in Logic & Proofs. This is a dynamic tutor interacting with students "intelligently" as follows: when students are trying to solve a proof construction problem in the Proof 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. The broad advice is, on further appeals, successively refined to a recommendation of the very next step that should be taken in the proof.