UBC Instructor David Gilbert is currently working on a BCcampus-funded project to add interactive activities to the popular open logic textbook forall x using an open Haskell framework called Carnap. Developed by Professor Graham Leach-Krouse at Kansas State, Carnap is an open framework that facilitates automated verification of formal proofs and allows instructors to build interactive web browser-based activities that support teaching and studying formal logic.
Post by David Gilbert, Philosophy Instructor, UBC, and Clint Lalonde, Project Manager Open Homework Systems, BCcampus
Once completed, the online resource will be used in UBC’s Philosophy 220 course — the largest core course in the Department of Philosophy at UBC — and will be made available as an open resource to be used by other logic instructors around the world.
The primary objective of the project is to create a free, online, and interactive symbolic logic text with an accompanying homework system that supports automated marking. Doing so will drastically reduce the money students need to spend learning logic, make the independent study of logic much easier, and allow universities and colleges to redistribute resources (like TA hours) so as to focus on pedagogically fruitful tasks.
In every logic course, a choice has to be made concerning what proof system will be introduced. Semantic tree systems are ideal for lower-level formal logic courses. They make explaining various fundamental, metatheoretical concepts much easier, and they shift the focus from syntactic manipulations to higher-level considerations. This allows students to focus more on fundamental concepts and also eases the transition between the study of introductory logic and more advanced topics in logic.
Recently, Professor Jonathan Ichikawa released the UBC version of forall x, an open textbook that makes use of logic trees (forall x was initially written by P.D. Magnus, a philosopher at SUNY Albany). However, while proof construction assistants/checkers have been created for other types of proof systems, there is a dearth of such systems for trees. This severely limits the reach of the UBC forall x text and hinders its use for independent study.
This project hopes to eliminate this gap by developing an in-browser widget for the construction of trees. Such an application will facilitate an online, interactive version of forall x. In addition, a homework system that builds on Carnap and automatically evaluates student-constructed tree proofs will be created. Such a system can be used for formal evaluations as well as individual practice.
The initial development phase of the in-browser tree-construction widget is already underway, and a beta version is available. It is hoped that a fully integrated online version of the UBC forall x book will be available to anybody who wants it by summer 2020.