Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

Research output: Contribution to journalJournal articleResearchpeer-review

2 Downloads (Pure)

Abstract

We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.
Original languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume354
Pages (from-to)71-85
ISSN2075-2180
DOIs
Publication statusPublished - 2022
Event10th International Workshop on Theorem proving components for Educational software - Carnegie Mellon University, Pittsburgh, United States
Duration: 11 Jul 202111 Jul 2021

Conference

Conference10th International Workshop on Theorem proving components for Educational software
LocationCarnegie Mellon University
Country/TerritoryUnited States
CityPittsburgh
Period11/07/202111/07/2021

Fingerprint

Dive into the research topics of 'Teaching Intuitionistic and Classical Propositional Logic Using Isabelle'. Together they form a unique fingerprint.

Cite this