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.
Courseware PackagesWe 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 fnatural 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 ixpressed 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.
Read more about Language, Proof and Logic and Tarski's World.
Heterogeneous Reasoning and the OpenboxOur investigation of formal heterogeneous reasonign 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 imtorducing a new representation.
You can read more about the Openbox.
Data Mining a Million ErrorsSince 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.
