Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

Jørgen Villadsen
(Technical University of Denmark)
Asta Halkjær From
(Technical University of Denmark)
Patrick Blackburn
(Roskilde University)

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.

In João Marcos, Walther Neuper and Pedro Quaresma: Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (ThEdu'21), (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021, Electronic Proceedings in Theoretical Computer Science 354, pp. 71–85.
Published: 8th February 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.354.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org