Overview   AProS   L & P   Proof Lab   Tutor   Truth Lab   Participants

automated proof search

OverviewConnectionsEvolutionDirectionReferences

Background and evolution

Wilfried Sieg in collaboration with Richard Scheines and Jonathan Pressler began the Carnegie Mellon Proof Tutor Project in 1986; Chris Walton was a tremendous support for programming an interface. The very basic ideas go actually back to 1985, when Sieg and Preston Covey discussed the underlying issues and the first steps were taken with Leslie Burkholder and Jonathan Miller. The state of the project is described in a publication for the first time in (Sieg and Scheines, 1992), Searching for proofs (in sentential logic). In the following, highlights of crucial steps in the development are presented together with the participants who contributed. This is a complex and big project, which can be carried out only in a collaborative way.

The theory of automated proof search for natural deduction proofs was articulated for sentential logic in the paper of Sieg and Scheines (1992). It was extended in 1992 to predicate logic by Sieg in Mechanisms and Search (aspects of proof theory) and refined in Sieg and Byrnes (1998), as well as in Byrnes' Ph.D. thesis Proof search and normal forms in natural deduction (1999). In collaboration with Saverio Cittadini, Sieg investigated proof search in intuitionistic logic and some systems of modal logic; most of the work was completed already in 1998, but published only in 2005. Ramyaa pursued the investigation of additional modal systems. Sieg with Clinton Field and Ian Kash used AProS as the logical base to prove abstract versions of Gödel's incompleteness theorems, respectively the Cantor-Bernstein theorem. Tyler Gibson has been working on an appropriate formulation of identity and automated proofs of additional theorems in set theory.

The implementation of the proof search algorithm (and of course the detailed algorithm itself) emerged slowly and in quite separate stages, not to speak languages. We started out in LISP, moved to C++, and are currently working in JAVA. Scheines and Pressler programmed the first version for sentential logic; Byrnes and Jesse Hughes took an important step towards an implementation for classical predicate logic. It was, however, Joseph Ramsey who restructured the algorithm most significantly into the current AProS architecture and re-wrote the "whole thing". Orlin Vakarelov, Kash and Gibson made further important improvements. One step was particularly helpful, namely to present the search in an appropriate interface, the Proof Display, so that one can examine proofs and their generation. Jessi Berkelhammer contributed here, in particular through the drawing of beautiful Fitch-diagrams.

The Proof Lab evolved out of the old CPT and is the work of Davin Lafon. It is a crucial practice space for students, who are taking the web-based course Logic & Proofs and have to construct natural deduction proofs. The course was designed and written by Dawn McLaughlin and Sieg; McLaughlin constructed all the quizzes and exercises with support and advice from Mark Ravaglia. The course is part of the Open Learning Initiative (OLI); the discussions in that group led to the inclusion of many Interactive Learning Environments (ILEs), which were constructed by McLaughlin with input from Lafon and Sieg. Ross Strader achieved their actual implementation. Quite a few "movies" were scripted and implemented cooperatively by Lafon, McLaughlin and Sieg. For the last two years, Conor Mayo-Wilson hascontributed to these developments.

The Proof Tutor has finally been developed. An early version was implemented by Perkins; that version has been throughly revised and restructured. It is being used now in Logic & Proofs. Obviously the tutoring is informed by the effective strategies of AProS and now uses the Proof Lab as its interactive platform. We have a marvelous laboratory for empirical investigations of the effectiveness of different presentations and teaching strategies. Scheines and Sieg investigated the effect of different proof presentations and associated strategies already for the old CPT; the results were published, appropriately enough in the journal "Interactive Learning Environments", volume 4, 1994, in their paper Computer environments for proof construction.

As mentioned above, such a large project can be carried out only with genuine collaboration. Everyone mentioned above has contributed to the AProS Project in other than the indicated ways, mostly through the weekly and lively group meetings. It is a pleasure to acknowledge the terrific support from the OLI group, in particular, from Candace Thille and Joel Smith. The list of others who have helped in vital ways during the almost twenty years of the project is long and includes Alex Smith, Bill Drozd, Matt Gramc, Bill Jerome, Michael Kohlhase, Ben Mashford, Iain McLaughlin, Spiros Papadimitrio, Ramyaa, John Rinderle, Raul Salinas, Carsten Schürmann, Willie Wheeler, Frank Wimberly. A number of colleagues outside Philosophy have been supportive, for example, Peter Andrews and Frank Pfenning at Carnegie Mellon, as well as Jörg Siekmann, Erica Melis, Christoph Benzmüller, and Serge Autexier in Saarbrücken.