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.

翻译：理论计算机科学领域的大型必修课程面临两个相互关联的挑战：帮助学生参与抽象材料的学习，以及在大规模教学中实现可靠的学生评估。本文介绍了LogicLab，这是一款专为滑铁卢大学CS 245“逻辑与计算”课程开发的轻量级计算工具包。该课程是计算机科学本科生的必修课，每年招收大量学生。其主要教学目标是帮助学生将课堂和作业中遇到的概念具体化。手写公式和证明步骤无法向学生提供即时的正确性反馈，这会减缓他们建立形式推理信心的速度，并使大规模一致评估变得更加困难。LogicLab通过允许学生在Racket环境中将公式、变换、子句、赋值和证明步骤作为计算对象进行操作来解决这一问题，直接基于他们一年级课程中积累的Scheme/Racket经验。LogicLab提供了解析和显示公式、应用等价变换、转换为范式、简化公式、处理赋值、应用归结规则、运行Davis-Putnam风格程序以及验证形式演绎步骤的工具。该系统比Coq或Lean等通用证明助手更轻量，并使用与课程一致的符号表示。它公开了可组合的函数，学生可以单独调用这些函数，或用于编程实现自己的自动化操作。本文介绍了LogicLab的设计原理、系统组织以及计划中的课程整合，将其作为使用计算工具支持大规模形式推理课程中参与度、概念具体性和更一致评估的实用模型。