Abstract:

Large foundational courses in theoretical computer science must address two simultaneous challenges: maintaining student engagement in highly abstract material and ensuring reliable assessment when large numbers of assignments must be graded by many teaching assistants. These challenges are particularly pronounced in large required courses where students do not arrive with a self-selected affinity for the subject. This paper describes the design of a lightweight software toolbox intended to address these issues in the second-year "Logic and Computation" course at the University of Waterloo. The course is required for all undergraduate computer science students and enrolls approximately 800 students annually.

The curriculum spans a broad range of topics, beginning with logical connectives and progressing through normal forms and resolution methods to first-order logic, natural-deduction proofs for Peano arithmetic, reasoning about program correctness, and proof of the undecidability of the halting problem. Historically the course relied entirely on handwritten proofs and manual grading. While this approach emphasizes rigorous reasoning, it creates two practical difficulties at scale. Many computer science students prefer exploratory and computational modes of learning over purely paper-based proofs, impacting engagement. At the same time, grading large numbers of handwritten proofs by a substantial and heterogeneous group of teaching assistants inevitably introduces variability in evaluation and feedback.

To address these issues, we developed a lightweight software toolbox that allows students to construct solutions through sequences of correct-by-construction operations. The system includes an expression editor for applying valid transformations to logical formulae, tools for checking equivalence and satisfiability in propositional logic, utilities for converting formulae into several normal forms, a resolution-based theorem prover including the Davis–Putnam procedure, and a proof checker for natural-deduction proofs in first-order logic. These components enable students to solve meaningful problems in logic while ensuring that intermediate steps remain logically valid.

The toolbox is implemented in Scheme, a language that all Waterloo computer science students learn in their first year, allowing students to compose primitives and experiment with reasoning processes programmatically. Unlike heavyweight proof assistants such as Coq or Lean, whose complexity would require significant instructional time, the toolbox adopts the same notation already used in the course. This design reduces cognitive overhead while supporting a computational environment in which students can experiment with logical constructions and obtain immediate feedback.

The tools were introduced on an optional basis during a recent offering of the course and are planned for broader integration in future iterations. The design illustrates how lightweight computational environments aligned with course notation can support engagement and consistent assessment in large-scale logic courses and may provide a practical model for other foundational subjects that combine formal reasoning with large enrollments.

Keywords:

Computer science education, learning technology, student engagement, scalable assessment, large-enrollment courses.