ProofBuddy: A Proof Assistant for Learning and Monitoring

Nadine Karsten; Frederik Krogsdal Jacobsen; Kim Jana Eiken; Uwe Nestmann; Jørgen Villadsen

doi:10.4204/EPTCS.382.1

ProofBuddy: A Proof Assistant for Learning and Monitoring

Nadine Karsten, Frederik Krogsdal Jacobsen, Kim Jana Eiken, Uwe Nestmann, Jørgen Villadsen

Technische Universität Berlin

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

124 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Proceedings of the Twelfth International Workshop on Trends in Functional Programming in Education
Editors	Elena Machkasova
Volume	382
Publisher	Open Publishing Association
Publication date	2023
Pages	1-21
DOIs	https://doi.org/10.4204/EPTCS.382.1
Publication status	Published - 2023
Event	12th International Workshop on Trends in Functional Programming in Education - Boston, United States Duration: 12 Jan 2023 → 12 Jan 2023 Conference number: 12

Conference

Conference	12th International Workshop on Trends in Functional Programming in Education
Number	12
Country/Territory	United States
City	Boston
Period	12/01/2023 → 12/01/2023

Series	Electronic Proceedings in Theoretical Computer Science
Volume	382
ISSN	2075-2180

Access to Document

10.4204/EPTCS.382.1Licence: CC BY

FulltextFinal published version, 969 KBLicence: CC BY

OpenUrl availability

Full text

Cite this

Karsten, Nadine ; Jacobsen, Frederik Krogsdal ; Eiken, Kim Jana et al. / ProofBuddy: A Proof Assistant for Learning and Monitoring. Proceedings of the Twelfth International Workshop on Trends in Functional Programming in Education. editor / Elena Machkasova. Vol. 382 Open Publishing Association, 2023. pp. 1-21 (Electronic Proceedings in Theoretical Computer Science, Vol. 382).

@inproceedings{9afc191e09eb489a99911fe0d6ec6a7b,

title = "ProofBuddy: A Proof Assistant for Learning and Monitoring",

abstract = "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{\textquoteright} 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 bycollecting 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.",

author = "Nadine Karsten and Jacobsen, {Frederik Krogsdal} and Eiken, {Kim Jana} and Uwe Nestmann and J{\o}rgen Villadsen",

year = "2023",

doi = "10.4204/EPTCS.382.1",

language = "English",

volume = "382",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "1--21",

editor = "Elena Machkasova",

booktitle = "Proceedings of the Twelfth International Workshop on Trends in Functional Programming in Education",

note = "12th International Workshop on Trends in Functional Programming in Education ; Conference date: 12-01-2023 Through 12-01-2023",

}

Karsten, N, Jacobsen, FK, Eiken, KJ, Nestmann, U & Villadsen, J 2023, ProofBuddy: A Proof Assistant for Learning and Monitoring. in E Machkasova (ed.), Proceedings of the Twelfth International Workshop on Trends in Functional Programming in Education. vol. 382, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, vol. 382, pp. 1-21, 12th International Workshop on Trends in Functional Programming in Education, Boston, Massachusetts, United States, 12/01/2023. https://doi.org/10.4204/EPTCS.382.1

ProofBuddy: A Proof Assistant for Learning and Monitoring. / Karsten, Nadine; Jacobsen, Frederik Krogsdal; Eiken, Kim Jana et al.
Proceedings of the Twelfth International Workshop on Trends in Functional Programming in Education. ed. / Elena Machkasova. Vol. 382 Open Publishing Association, 2023. p. 1-21 (Electronic Proceedings in Theoretical Computer Science, Vol. 382).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - ProofBuddy: A Proof Assistant for Learning and Monitoring

AU - Karsten, Nadine

AU - Jacobsen, Frederik Krogsdal

AU - Eiken, Kim Jana

AU - Nestmann, Uwe

AU - Villadsen, Jørgen

N1 - Conference code: 12

PY - 2023

Y1 - 2023

N2 - 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 bycollecting 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.

AB - 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 bycollecting 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.

U2 - 10.4204/EPTCS.382.1

DO - 10.4204/EPTCS.382.1

M3 - Article in proceedings

VL - 382

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 1

EP - 21

BT - Proceedings of the Twelfth International Workshop on Trends in Functional Programming in Education

A2 - Machkasova, Elena

PB - Open Publishing Association

T2 - 12th International Workshop on Trends in Functional Programming in Education

Y2 - 12 January 2023 through 12 January 2023

ER -

Karsten N, Jacobsen FK, Eiken KJ, Nestmann U, Villadsen J. ProofBuddy: A Proof Assistant for Learning and Monitoring. In Machkasova E, editor, Proceedings of the Twelfth International Workshop on Trends in Functional Programming in Education. Vol. 382. Open Publishing Association. 2023. p. 1-21. (Electronic Proceedings in Theoretical Computer Science, Vol. 382). doi: 10.4204/EPTCS.382.1

ProofBuddy: A Proof Assistant for Learning and Monitoring

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this