A theorem prover for scientific and educational purposes
- We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education.
| Author details: | Mario FrankORCiDGND, Christoph Kreitz |
|---|---|
| DOI: | https://doi.org/10.4204/EPTCS.267.4 |
| ISSN: | 2075-2180 |
| Title of parent work (English): | Electronic proceedings in theoretical computer science |
| Publisher: | Open Publishing Association |
| Place of publishing: | Sydney |
| Publication type: | Other |
| Language: | English |
| Date of first publication: | 2018/03/05 |
| Publication year: | 2018 |
| Release date: | 2022/02/17 |
| Issue: | 267 |
| Number of pages: | 11 |
| First page: | 59 |
| Last Page: | 69 |
| Organizational units: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
| DDC classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 000 Informatik, Informationswissenschaft, allgemeine Werke |
| Peer review: | Referiert |
| Publishing method: | Open Access / Gold Open-Access |
| DOAJ gelistet | |
| License (English): |  Creative Commons - Namensnennung - Nicht-kommerziell - Weitergabe unter gleichen Bedingungen 3.0 Unported |
