The Automated Proof Search (AProS) Project

at Carnegie Mellon

Project Participants

AProS
Proof Tutor
Proof Lab
Logic and Proofs

The AProS Project consists of four separate, but deeply integrated parts, namely, the central proof search engine AProS, the proof tutor, the proof laboratory, and the web-based course Logic & Proofs. It is a project that combines proof theoretic investigation of natural deduction calculi, the discovery and implementation of efficient proof search methods with a novel, web-based presentation of predicate logic. The goal is to help students uncover the structure of logical arguments and construct proofs in the proof lab. At the same time it serves as a framework to investigate empirical questions on the efficacy of particular teaching strategies and on the adequacy of psychological theories of mental proofs.