### Abstract

The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle but 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. In fact, 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.

Original language | English |
---|---|

Publication date | 2018 |

Number of pages | 6 |

Publication status | Published - 2018 |

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 | United Kingdom |

City | Oxford |

Period | 18/07/2018 → 18/07/2018 |

Internet address |

## Cite this

Schlichtkrull, A., Villadsen, J., & From, A. H. (2018).

*Students' Proof Assistant (SPA)*. Paper presented at International Workshop on Theorem proving components for Educational software , Oxford , United Kingdom.