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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.354.6 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |