# Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

arXiv: https://arxiv.org/abs/2202.03567 · HTML: https://mlsanity.com/paper/2202.03567/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Feb 2022.

## Built on by (most cited first, 3 of 3)

- [LogicLearner: A Tool for the Guided Practice of Propositional Logic Proofs](https://mlsanity.com/paper/2503.19280/) (2025)
- [On Exams with the Isabelle Proof Assistant](https://mlsanity.com/paper/2303.05866/) (2023)
- [Teaching Higher-Order Logic Using Isabelle](https://mlsanity.com/paper/2404.05458/) (2024)

## Abstract (arXiv)

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.