A Theorem Prover for Scientific and Educational Purposes

TL;DR

This paper introduces a prototype theorem prover designed for educational use, supporting untyped lambda calculus to aid students and researchers in understanding functional programming and theorem proving.

Contribution

It presents a novel integrated reasoning environment tailored for educational purposes, combining proof assistance with automated theorem proving functionalities.

Findings

Supports understanding of untyped lambda calculus

Aids students in learning functional programming

Addresses challenges in developing educational theorem proving tools

Abstract

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.