A Theorem Prover for Scientific and Educational Purposes

Mario Frank
(University of Potsdam, Institute for Computer Science, Potsdam, Germany)
Christoph Kreitz
(University of Potsdam, Institute for Computer Science, Potsdam, Germany)

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.

In Pedro Quaresma and Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science 267, pp. 59–69.
Published: 2nd March 2018.

ArXived at: https://dx.doi.org/10.4204/EPTCS.267.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org