automated proof search
Project Director: Wilfried Sieg
Research Staff:Davin Lafon, Dawn McLaughlin, Tyler Gibson
Research Collaborators: Joseph Ramsey, Klaus Sutner, Christian Schunn
Research Associates (current):Conor Mayo-Wilson, Einam Livnat, Adam Conkey
The AProS Project consists of five separate, but deeply integrated parts, namely, the central proof search engine AProS the Proof Tutor, the Proof Lab, the Truth Lab and the web-based course Logic & Proofs. It is a project that combines proof theoretic investigations 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, but also to define counterexamples (via semantic tableaux or truth trees) in the Truth 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.
The connections between the parts are described. Each part has required and is still requiring extensive development. The projects evolution is discussed, but also the research direction in which it is moving. Many people have helped to bring the project to its current state; their roles are briefly described in the background and evolution section. Papers presenting some of the developments can be found in the references section.
Beginning in 2006, the project has been extended to go beyond pure logic and cover elementary set theory, but also computability. That is described more in the paper Strategic Thinking
The project has received financial support from the Buhl Foundation, the National Science Foundation, the Qatar Foundation and the Hewlett Foundation. Internally, the University, the College of Humanities & Social Sciences and the Department of Philosophy have provided funds. From 2006 to 2010 the AProS project was supported by grant 0618806 from the National Science Foundation (Mathematical Science Division, CCLI - Expansion Projects).