Isabelle/HOL as a Meta-Language for Teaching Logic

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

16 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings 9th International Workshop on Theorem Proving Components for Educational Software
EditorsJ. Marcos, W. Neuper, P. Quaresma
PublisherOpen Publishing Association
Publication date2020
Pages18–34
DOIs
Publication statusPublished - 2020
Event9th International Workshop on Theorem Proving Components for Educational Software - Virtual event, Paris, France
Duration: 29 Jun 202029 Jun 2020

Conference

Conference9th International Workshop on Theorem Proving Components for Educational Software
LocationVirtual event
CountryFrance
CityParis
Period29/06/202029/06/2020
SeriesElectronic Proceedings in Theoretical Computer Science
Volume328
ISSN2075-2180

Fingerprint Dive into the research topics of 'Isabelle/HOL as a Meta-Language for Teaching Logic'. Together they form a unique fingerprint.

Cite this