Isabelle/HOL as a Meta-Language for Teaching Logic

Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Abstract

Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus that uses our Sequent Calculus Verifier (SeCaV). We describe each formalization in turn, concentrating on how we used them in our teaching, and commenting on features that are interesting or useful from a logic education perspective. In the conclusion, we reflect on the lessons learned and where they might lead us next.
OriginalsprogEngelsk
Titel Proceedings 9th International Workshop on Theorem Proving Components for Educational Software (ThEdu'20)
Antal sider17
Udgivelses stedWaterloo
ForlagOpen Publishing Association
Publikationsdato2020
Sider18-34
DOI
StatusUdgivet - 2020
Begivenhed9th International Workshop on
Theorem Proving Components for Educational Software
Paris, France, 29th June 2020
- Paris, Frankrig
Varighed: 29 jun. 2020 → …
Konferencens nummer: 9

Konference

Konference9th International Workshop on
Theorem Proving Components for Educational Software
Paris, France, 29th June 2020
Nummer9
LandFrankrig
ByParis
Periode29/06/2020 → …
NavnElectronic Proceedings in Theoretical Computer Science
Nummer328
ISSN2075-2180

Citer dette