Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

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

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

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.

OriginalsprogEngelsk
TidsskriftElectronic Proceedings in Theoretical Computer Science, EPTCS
Vol/bind354
Sider (fra-til)71-85
Antal sider15
ISSN2075-2180
DOI
StatusUdgivet - 8 feb. 2022
Begivenhed10th International Workshop on Theorem Proving Components for Educational Software, ThEdu 2021 - Pittsburgh, USA
Varighed: 11 jul. 2021 → …

Konference

Konference10th International Workshop on Theorem Proving Components for Educational Software, ThEdu 2021
Land/OmrådeUSA
ByPittsburgh
Periode11/07/2021 → …

Citer dette