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.
|Journal||Electronic Proceedings in Theoretical Computer Science, EPTCS|
|Publication status||Published - 2022|
|Event||10th International Workshop on Theorem proving components for Educational software - Carnegie Mellon University, Pittsburgh, United States|
Duration: 11 Jul 2021 → 11 Jul 2021
|Conference||10th International Workshop on Theorem proving components for Educational software|
|Location||Carnegie Mellon University|
|Period||11/07/2021 → 11/07/2021|