Students' Proof Assistant (SPA)

Anders Schlichtkrull
(Technical University of Denmark)
Jørgen Villadsen
(Technical University of Denmark)
Andreas Halkjær From
(Technical University of Denmark)

The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In addition we conjecture that a good way to teach structured proving is with a concrete prover where the connection between semantics, proof system, and prover is clear. The proofs in Lamport's TLAPS proof assistant have a very similar structure to those in the declarative prover SPA. To illustrate this we compare a proof of Pelletier's problem 43 in TLAPS, Isabelle/Isar and SPA. We also consider Pelletier's problem 34, also known as Andrews's Challenge, where students are encouraged to develop their own justification function and thus obtain a lot of insight into the proof assistant. Although SPA is fully functional we have so far only used it in a few educational scenarios.

In Pedro Quaresma and Walther Neuper: Proceedings 7th International Workshop on Theorem proving components for Educational software (ThEdu'18), Oxford, United Kingdom, 18 july 2018, Electronic Proceedings in Theoretical Computer Science 290, pp. 1–13.
Published: 1st April 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: