Journal article · Preprint article
Students’ Proof Assistant (SPA)
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.
Language: | English |
---|---|
Publisher: | Open Publishing Association |
Year: | 2019 |
Pages: | 1-13 |
Proceedings: | International Workshop on Theorem proving components for Educational software |
ISSN: | 20752180 |
Types: | Journal article and Preprint article |
DOI: | 10.4204/EPTCS.290.1 |
ORCIDs: | Schlichtkrull, Anders , Villadsen, Jørgen and From, Andreas Halkjær |