Waterproof: Educational Software for Learning How to Write Mathematical Proofs
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2022
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910400440696832 |
|---|---|
| author | Wemmenhove, Jelle Arends, Dick Beurskens, Thijs Bhaid, Maitreyee McCarren, Sean Moraal, Jan Garrido, Diego Rivera Tuin, David Vassallo, Malcolm Wils, Pieter Portegies, Jim |
| author_facet | Wemmenhove, Jelle Arends, Dick Beurskens, Thijs Bhaid, Maitreyee McCarren, Sean Moraal, Jan Garrido, Diego Rivera Tuin, David Vassallo, Malcolm Wils, Pieter Portegies, Jim |
| contents | In order to help students learn how to write mathematical proofs, we adapt the Coq proof assistant into an educational tool we call Waterproof. Like with other interactive theorem provers, students write out their proofs inside the software using a specific syntax, and the software provides feedback on the logical validity of each step. Waterproof consists of two components: a custom proof language that allows formal, machine-verified proofs to be written in a style that closely resembles handwritten proofs, and a custom editor that allows these proofs to be combined with formatted text to improve readability. The editor can be used for Coq documents in general, but also offers special features designed for use in education. Student input, for example, can be limited to specific parts of the document to prevent exercises from being accidentally deleted. Waterproof has been used to supplement teaching the Analysis 1 course at Eindhoven University of Technology (TU/e) for the last four years. Students started using the specific formulations of proof steps from the custom proof language in their handwritten proofs; the explicit phrasing of these sentences helped to clarify the logical structure of their arguments. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2211_13513 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Waterproof: Educational Software for Learning How to Write Mathematical Proofs Wemmenhove, Jelle Arends, Dick Beurskens, Thijs Bhaid, Maitreyee McCarren, Sean Moraal, Jan Garrido, Diego Rivera Tuin, David Vassallo, Malcolm Wils, Pieter Portegies, Jim History and Overview In order to help students learn how to write mathematical proofs, we adapt the Coq proof assistant into an educational tool we call Waterproof. Like with other interactive theorem provers, students write out their proofs inside the software using a specific syntax, and the software provides feedback on the logical validity of each step. Waterproof consists of two components: a custom proof language that allows formal, machine-verified proofs to be written in a style that closely resembles handwritten proofs, and a custom editor that allows these proofs to be combined with formatted text to improve readability. The editor can be used for Coq documents in general, but also offers special features designed for use in education. Student input, for example, can be limited to specific parts of the document to prevent exercises from being accidentally deleted. Waterproof has been used to supplement teaching the Analysis 1 course at Eindhoven University of Technology (TU/e) for the last four years. Students started using the specific formulations of proof steps from the custom proof language in their handwritten proofs; the explicit phrasing of these sentences helped to clarify the logical structure of their arguments. |
| title | Waterproof: Educational Software for Learning How to Write Mathematical Proofs |
| topic | History and Overview |
| url | https://arxiv.org/abs/2211.13513 |