The Openproof Project at CSLI: Research

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.

Courseware Packages

We have developed the following courseware packages, aimed at different aspects of the undergraduate logic curriculum:

...Read more about Language, Proof and Logic and Tarski's World.

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.


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.