Abstract
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.
| Original language | English |
|---|---|
| Journal | Electronic Proceedings in Theoretical Computer Science |
| Volume | 290 |
| Pages (from-to) | 1–13 |
| ISSN | 2075-2180 |
| DOIs | |
| Publication status | Published - 2019 |
| Event | International Workshop on Theorem proving components for Educational software - Oxford , United Kingdom Duration: 18 Jul 2018 → 18 Jul 2018 http://www.uc.pt/en/congressos/thedu/thedu18/programme |
Conference
| Conference | International Workshop on Theorem proving components for Educational software |
|---|---|
| Country/Territory | United Kingdom |
| City | Oxford |
| Period | 18/07/2018 → 18/07/2018 |
| Internet address |