OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912367756967936 |
|---|---|
| author | Perháč, Ján Novotný, Samuel Chodarev, Sergej Kristensen, Joachim Tilsted Tveito, Lars Shturmov, Oleks Thomsen, Michael Kirkedal |
| author_facet | Perháč, Ján Novotný, Samuel Chodarev, Sergej Kristensen, Joachim Tilsted Tveito, Lars Shturmov, Oleks Thomsen, Michael Kirkedal |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_05987 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs Perháč, Ján Novotný, Samuel Chodarev, Sergej Kristensen, Joachim Tilsted Tveito, Lars Shturmov, Oleks Thomsen, Michael Kirkedal Logic in Computer Science F.3.0; F.4.1; I.2.3 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. |
| title | OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs |
| topic | Logic in Computer Science F.3.0; F.4.1; I.2.3 |
| url | https://arxiv.org/abs/2505.05987 |