A Computational Toolkit for Engagement and Scalable Assessment in a Large Logic Course
2026-06-01 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors created LogicLab, a simple computer tool to help big classes of computer science students better understand and practice logic concepts. Since handwritten work doesn't give instant feedback, LogicLab lets students work directly with logical formulas and proofs on a computer, using a language they already know. This helps students learn more confidently and makes grading easier and fairer for teachers. The tool is simpler than big proof systems and is designed to fit naturally into the course curriculum.
formal reasoningproof assistantlogic formulasequivalence transformationsnormal formsresolution ruleDavis-Putnam procedureRacket programming languagestudent assessmentcomputational toolkit
Authors
Stephen M. Watt
Abstract
Large required courses in theoretical computer science face two related challenges: helping students engage with abstract material and supporting reliable student assessment at scale. This paper describes LogicLab, a lightweight computational toolkit developed for CS 245, Logic and Computation, at the University of Waterloo. The course is required for undergraduate computer science students and serves a large annual cohort. The main pedagogical objective is to help students concretize the ideas they encounter in lectures and assignments. Handwritten formulas and proof steps do not give students immediate correctness feedback. This can slow their development of confidence in formal reasoning and makes assessment harder to apply consistently at scale. LogicLab addresses this by allowing students to manipulate formulas, transformations, clauses, valuations, and proof steps as computational objects in Racket, building directly on their Scheme/Racket experience from the first-year curriculum. LogicLab provides tools for parsing and displaying formulas, applying equivalence transformations, converting to normal forms, simplifying formulas, working with valuations, applying resolution rules, running a Davis-Putnam style procedure, and verifying formal deduction steps. The system is lighter than a general proof assistant such as Coq or Lean and uses notation aligned with the course. It exposes composable functions students can invoke individually or use to program their own automations. The paper presents the design rationale, system organization, and planned course integration of LogicLab as a practical model for using computational tools to support engagement, conceptual concreteness, and more consistent assessment in large formalreasoning courses.