Students' Proof Assistant (SPA)

Anders Schlichtkrull, Jørgen Villadsen, Asta Halkjær From

Research output: Contribution to conferencePaperResearchpeer-review

212 Downloads (Pure)

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 languageEnglish
Publication date2018
Number of pages6
Publication statusPublished - 2018
EventInternational Workshop on Theorem proving components for Educational software - Oxford , United Kingdom
Duration: 18 Jul 201818 Jul 2018
http://www.uc.pt/en/congressos/thedu/thedu18/programme

Conference

ConferenceInternational Workshop on Theorem proving components for Educational software
Country/TerritoryUnited Kingdom
CityOxford
Period18/07/201818/07/2018
Internet address

Fingerprint

Dive into the research topics of 'Students' Proof Assistant (SPA)'. Together they form a unique fingerprint.

Cite this