

automated proof search 

Proof TutorThe Proof Tutor is the bridge between AProS and the Proof Lab. It enables students who are stuck on a proof to receive hints, dynamically obtained from Generated Proofs. If a student requests a hint, AProS will construct a complete proof, which the Tutor analyzes. The Tutor then provides hints to construct the proof using the efficient and natural strategies employed by Proof Generator. The first hint provided at any point in the proof is general strategic one, and subsequent hints provide more concrete advice as to how to proceed. The last hint in the sequence recommends that the student take a particular step in the proof construction. This implementation is informed by pedagogical concerns relating to both computerbased tutors and logic education. We are also considering broad theoretical issues in the intersection of logic and cognitive psychology, such as the relation between formal and informal reasoning and the transfer of strategic argumentation skills. 