Overview   Generator   L & P   Proof Tutor   Proof Lab   Participants

automated proof search

OverviewConnectionsEvolutionDirectionReferences

Overview

Project Director: Wilfried Sieg

Research Staff: Joseph Ramsey, Davin Lafon, Dawn McLaughlin, Tyler Gibson

Research Collaborators: Klaus Sutner, Marsha Lovett, Kurt van Lehn

Research Assistants (current):Douglas Perkins, Alex Smith, Michael Warren

The AProS Project consists of four separate, but deeply integrated parts, namely, the central proof search engine Proof Generator the Proof Tutor, the Proof 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. 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 section. Papers presenting some of the developments can be found in the references section.

The project has received financial support from the Buhl Foundation, the National Science Foundation, and the Hewlett Foundation; internally, the University, the College of Humanities & Social Sciences and the Department of Philosophy have provided funds. Currently, the AProS project is supported by grant 0618806 from the National Science Foundation (Mathematical Science Division, CCLI - Expansion Projects).