Nadine Karsten (Technische Universität Berlin) |
Frederik Krogsdal Jacobsen (Technical University of Denmark) |
Kim Jana Eiken (Technische Universität Berlin) |
Uwe Nestmann (Technische Universität Berlin) |
Jørgen Villadsen (Technical University of Denmark) |
Proof competence, i.e. the ability to write and check (mathematical) proofs, is an important skill in Computer Science, but for many students it represents a difficult challenge. The main issues are the correct use of formal language and the ascertainment of whether proofs, especially the students' own, are complete and correct. Many authors have suggested using proof assistants to assist in teaching proof competence, but the efficacy of the approach is unclear. To improve the state of affairs, we introduce ProofBuddy: a web-based tool using the Isabelle proof assistant which enables researchers to conduct studies of the efficacy of approaches to using proof assistants in education by collecting fine-grained data about the way students interact with proof assistants. We have performed a preliminary usability study of ProofBuddy at the Technical University of Denmark. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.382.1 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |