The Openproof Project at CSLI: Research

Openproof Day 2009

We would like to invite you to attend Openproof Day 2009 at Stanford University's Center for the Study of Language and Information, on March 27 2009.

All talks will take place at CSLI's Cordura Hall, Room 100. Directions to CSLI can be found here.

Openproof day will be a day of events discussing a variety of topics related to the work of the project, including:


8:30‒9:30: An Overview of the Openproof Project

9:30‒10:00: Coffee

10:00‒11:00: Language, Proof and Logic

In this talk I will introduce the Language Proof and Logic (LPL) courseware package. The courseware package consists of a textbook, three desktop applications used by students to complete work, and an automated grading service which serves as a teaching assistant able to assess student work, available 24/7. Language, Proof and Logic was first published in 1999. As we approach its tenth anniversary, I will reflect on our experiences with this package, and indicate our plans for a new edition which will include a revision to some of the material covered in the text, and improved software support for some of the material in the course. In particular we plan to add support in the proof environment, Fitch, for induction over the natural numbers and the use of lemmas, and allow instructors to set their own exercises for grading by the Grade Grinder.

11:00‒12:00: A Panel discussion with Language, Proof and Logic Instructors

12:00‒1:30: Lunch

1:30‒2:30: Seeing how students really err: Data mining the Grade Grinder corpus

The ease with which a student can translate a natural language sentence into formal logic depends, amongst other things, on just how that natural language sentence is phrased. In the talk I will report findings from pilot studies where we used a very large dataset to provide empirical evidence for specific characteristics of natural language problem statements that frequently lead to students making mistakes.

The dataset consists of student-generated solutions to exercises in Language, Proof and Logic (LPL). Students may submit answers to LPL's exercises to The Grade Grinder, an automated assessment system that has assessed approximately 1.8 million submissions of work by more than 38,000 individual students.

We have developed a taxonomy of the types of errors that students make, and implemented tools for automatically classifying student errors into these categories. In the talk I will outline the taxonomy and show examples. We believe that a large class of errors can be explained in terms of mal-rules that capture student misunderstandings of how to translate natural language expressions into logical connectives.

We have also looked at how students construct diagrammatic representations of information expressed in natural language sentences. This reveals misunderstandings that would not otherwise be apparent - diagram construction seems to test students' understanding in ways that translation into first-order logic does not.

The talk will conclude by considering the implications for improving Grade Grinder's feedback to students specifically, and logic teaching more generally. We hope that the findings will also allow us to construct exercises that focus on important aspects of the translation process, and allow us to avoid exercises that are difficult for unintended reasons.

2:30‒3:00: Coffee

3:00‒4:00: Kripke's World, a review

Expressions like "possible that..." or "knows that..." that qualify the truth of a sentence are called modals. Modal logic is concerned with the meanings and logical properties of modals. Kripke's World is a new courseware package designed to supplement an introductory course on modal logic. In this talk, I will introduce Kripke's World and describe how to integrate it into a modern course on modal logic.

4:00‒5:00: Heterogeneous Reasoning, Hyperproof and the Openbox

During the 1990s, Barwise and Etchemendy developed the theory of formal heterogeneous deduction: logically valid inference that involves information expressed using multiple different representations — sentences of English together with street maps, for example. At CSLI's Openproof Project, we have since been generalizing both the theory and the implementation to allow applications in a wide variety of domains. On the theoretical side, we have identified features of heterogeneous reasoning which occur in everyday domains, but which do not correspond to logical deductions. Examples here include applications in design, where a desired design may not be a logical consequence of some initial information, but rather is preferred based on notions of aesthetics, cost or other non-logical features of the design domain. The general principles of information flow through a structured argument remain the same in both formal and informal contexts. On the implementation side, we have designed the Openproof architecture, an application framework for building heterogeneous reasoning systems which permits "plug-ins". In this talk we will describe our generalized theory of heterogeneous reasoning motivated by examples from design and by problems taken from GRE and SAT tests. We will demonstrate a variety of applications based on the Openproof framework to show the range of heterogeneous reasoning applications which may be built using the system.

Who Should Attend?

We particularly encourage you to attend if:

  1. you have adopted one of our courseware packages for a class (we want to hear how it works for you)
  2. you are considering adopting one of our courseware packages (we want you to hear from instructors who have)
  3. you are interested in logic education (we want you to hear about findings from our data mining studies)
  4. you are interested in heterogeneous reasoning (we want to tell you more about our Openbox project)

How to Register

Attendance is free and open to the public. Please let us know in advance if you plan to attend by sending mail to .

We can help to organise accommodation for those traveling to the meeting. We regret that we are unable to provide funding to attend this event.

A Helpful Suggestion from Google