OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs

TL;DR

OnlineProver addresses the challenge of teaching formal proofs in computer science by delivering a lightweight, domain-specific proof tool that guides students through Gentzen-style derivations with inline feedback. It avoids full-blown proof assistants to keep syntax approachable, requiring students to construct complete derivations while the engine checks correctness. The paper presents the tool design, an initial classroom deployment with 165 students, and a mixed-methods evaluation showing moderate usability (SUS ≈ 67) and positive perception of feedback, alongside ongoing learning challenges tied to formal methods. Findings indicate that OnlineProver supports trial-and-error exploration and reflection but pen-and-paper proofs remain more effective for deep learning; the authors propose future work including two domain-specific languages to broaden the tool's scope and automate assessments while preserving student agency.

Abstract

OnlineProver is an interactive proof assistant tailored for the educational setting. Its main features include a user-friendly interface for editing and checking proofs. The user interface provides feedback directly within the derivation, based on error messages from a proof-checking web service. A basic philosophy of the tool is that it should aid the student while still ensuring that the students construct the proofs as if they were working on paper. We gathered feedback on the tool through a questionnaire, and we conducted an intervention to assess its effectiveness for students in a classroom setting, alongside an evaluation of technical aspects. The initial intervention showed that students were satisfied with using OnlineProver as part of their coursework, providing initial confirmation of the learning approach behind it. This gives clear directions for future developments, with the potential to find and evaluate how OnlineProver can improve the teaching of natural deduction.

Figures (12)

• Figure 1: An example of interacting with OnlineProver.
• Figure 2: Exercise 6-d from onlineprover.com.
• Figure 3: An example of an incorrectly applied rule.
• Figure 4: An example of the error with a partially written derivation.
• Figure 5: An examples of a closed proof.