OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs
J\'an Perh\'a\v{c} (Technical University of Ko\v{s}ice, Slovakia), Samuel Novotn\'y (Technical University of Ko\v{s}ice, Slovakia), Sergej Chodarev (Technical University of Ko\v{s}ice, Slovakia), Joachim Tilsted Kristensen (University of Oslo, Norway)
TL;DR
OnlineProver is an interactive visualization tool designed to enhance teaching of formal proofs, providing real-time feedback and supporting students in constructing proofs effectively in an educational setting.
Contribution
The paper introduces OnlineProver, a novel proof assistant with a user-friendly interface and integrated feedback, tailored specifically for educational use in teaching formal proofs.
Findings
Students reported high satisfaction with OnlineProver.
Initial intervention suggests improved proof construction learning.
Technical evaluation confirms tool's usability and effectiveness.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.