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:

- Presentation of existing courseware packages including plans for future improvements,
- Discussion with instructors on the use of existing courseware packages,
- Presentation of courseware packages for future release,
- Presentation of recent research in data mining student work in logic.

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

**John Etchemendy**, Philosophy, Stanford University, USA

**9:30‒10:00: Coffee**

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

**Dave Barker-Plummer**, CSLI, Stanford University, USA

Download LPL slides (pdf)

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**

**S. Marc Cohen**, Philosophy (emeritus), University of Washington, USA**Holly Groover**, Philosophy, University of South Carolina, USA**Cindy Stern**, Philosophy, California State University Northridge, USA

**12:00‒1:30: Lunch**

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

**Richard Cox**, Informatics, University of Sussex, UK

Download Cox slides (pdf)

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**

**Eric Pacuit**, Philosophy, Stanford University, USA

Download Pacuit slides (pdf)

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**

**Dave Barker-Plummer**, CSLI, Stanford University, USA

Download Heterogeneous Reasoning slides (pdf)

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.

We particularly encourage you to attend if:

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

Attendance is free and open to the public. Please let us know in advance if you plan to attend by sending mail to dbp -at- stanford -dot- edu.

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.