The Openproof Project
The Openproof project at Stanford's Center for the Study of Language and Information (CSLI) is concerned with the application of software to problems in logic. Since the early 1980's we have been developing applications in logic education which are both innovative and effective. The development of these courseware packages has in turn informed and influenced our research agenda.
We are currently engaged in a project to understand the difficulties that students encounter when learning logic. Our approach to this task is to use data mining techniques on a large corpus of student work that we have gathered through our Internet-based grading service over the past ten years. The corpus currently consists of over 2.75 million submissions of work from more than 55,000 individual students.
A second project involves the investigation of the logics of diagrammatic and heterogeneous reasoning. Logic has traditionally been concerned with deduction using information expressed as sentences. In this project we are concerned with developing formal and informal systems for logical reasoning with diagrams alone, and in heterogeneous contexts where diagrams and sentences are used together to represent information about a reasoning task.
We have developed the following courseware packages, aimed at different aspects of the undergraduate logic curriculum:
- Language, Proof and Logic — a complete textbook for an introductory course in first-order logic covering propositional and first-order logic through completeness and soundness, with sections on set theory and induction. The courseware package includes Fitch, a proof environment for constructing natural deduction proofs, Boole an application for constructing truth tables and Tarski's World an environment for investigating the semantics of first-order sentences in the blocks world. The package also contains access to our innovative Internet-based grading service The Grade Grinder.
- Tarski's World — a book of exercises aimed at introducing the semantics of first-order logic though our application Tarski's World. A revised and expanded edition with access to our innovative Internet-based grading service The Grade Grinder was published in 2008.
- Hyperproof — a courseware package aimed at teching formal heterogeneous reasoning—reasoning in which the premises and conclusions are expressed in multiple representations, not just first-order sentences as in conventional formal logic. The Hyperproof package is currently out of print.
- The Language of First-Order Logic — a full introductory course for first-order logic with software support for learning first-order smeantics using out Tarski's World application. The Language of First-Order Logic is superceded by Language Proof and Logic and is currently out of print.
- Turing's World — a book of exercises for teaching computability theory using a Turing mahine simulator Turing's World. The Turing's World package is currently out of print.
Heterogeneous Reasoning and the Openbox
Our investigation of formal heterogeneous reasoning and the development of the Hyperproof package has led us to realise that there are many applications of heterogeneous reasoning, both in pedagogical settings and for real-world applications. We are currently developing the Openbox, an application for general heterogeneous reasoning with a plug-in architecture. Users may develop heterogeneous reasoning applications by plugging together components which implement representations of their choice. The Openbox will maintain the structure of the proof while the individual components will be responsible for providing representation-specific features.
The implementation of a representation require provision of a data-structure implementing the representation itself, a editor which enables the construction and modification of such structures, and an engine, which contains the specification of inference rules specific to that representation. heterogeneous inference engines can be implemented with knowledge only of the structure of the representations involved. The Openbox will thus permit the rapid development of heterogeneous reasoning applications by providing common heterogeneous proof maintenance services to its plugin components, reducing the work for developers interested in introducing a new representation.
You can read more about the Openbox.
Data Mining a Million Errors
Since the introduction of The Grade Grinder in 1999 we have collected a very corpus of student solutions to the exercises in the Language, Proof and Logic package. As of the beginning of 2008, this corpus consists of more than 1.8 million student submissions, most involving more than one exercise from the textbook. From 2008 we will be collecting a similar corpus of solutions to the exercises in the revised and expanded edition of Tarski's World.
Naturally, not all of the submissions made by our students are correct, and we have embarked on a data mining project to investigate the range of errors made by students when completing these exercises. We will use the results of this study to improve the feedback provided by The Grade Grinder, and also to better understand the stumbling blocks encountered by students as they are introduced to formal logic. We anticipate that the results of the study will be of interest to all logic educators, independent of their use of our courseware.
You can read more about this Data Mining Project.
On March 27, 2009 we held Openproof Day. On this page you can find slides for the talks, which concerned all aspects of our project.