Abstract
A novel approach to design an inclusive and accessible mathematical learning environment is presented: The technology of theorem proving shall be employed to support a student in solving mathematical problems by giving hints to him/her based on formal proofs of each step in a calculation. The system shall be made accessible by making use of the built-in accessibility coming with VSCode, a standard editor used as front-end for the theorem prover Isabelle.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
- 5.
The formalisations use brackets “[” and “]” denoting lists as usual in functional programming. Some inner lists, actually, are interpreted as sets.
References
Back, R.J.: Structured derivations as a unified proof style for teaching mathematics. TUCS Technical Report 949, TUCS - Turku Centre for Computer Science, Turku, Finland (2009)
Karl, N.: Develo** an Inclusive Approach for Representing Mathematical Formulas. Master’s thesis, Hagenberg University of Applied Sciences, Linz, Austria (2016). https://static.miraheze.org/isacwiki/0/02/Masterthesis_NatalieKarl.pdf
Krempler, A., Neuper, W.: Prototy** systems that explain themselves for education. In: Quaresma, P., Neuper, W. (eds.) Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017. Electronic Proceedings in Theoretical Computer Science, vol. 267, pp. 89–107. Open Publishing Association (2018). https://doi.org/10.4204/EPTCS.267.6, https://arxiv.org/abs/1803.01470v1
Mahringer, M.: Formula Editors for TP-based Systems. State of the Art and Prototype Implementation in ISAC. Master’s thesis, University of Applied Sciences, Hagenberg, Austria (2018). https://static.miraheze.org/isacwiki/d/d7/Mmahringer-master.pdf
Paulson, L.C., Nipkow, T., Wenzel, M.: From LCF to Isabelle/HOL. Formal Aspects Comput. 31, 675–698 (2019). https://doi.org/10.1007/s00165-019-00492-1
Wenzel, M.: Isabelle/Isar – a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof – Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10, no. 23. University of Białystok (2007). https://www21.in.tum.de/~wenzelm/papers/isar-framework.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Stöger, B., Miesenberger, K., Neuper, W., Wenzel, M., Neumayr, T. (2022). Designing an Inclusive and Accessible Mathematical Learning Environment Based on a Theorem Prover. In: Miesenberger, K., Kouroupetroglou, G., Mavrou, K., Manduchi, R., Covarrubias Rodriguez, M., Penáz, P. (eds) Computers Hel** People with Special Needs. ICCHP-AAATE 2022. Lecture Notes in Computer Science, vol 13341. Springer, Cham. https://doi.org/10.1007/978-3-031-08648-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-031-08648-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-08647-2
Online ISBN: 978-3-031-08648-9
eBook Packages: Computer ScienceComputer Science (R0)