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.
| Original language | English |
|---|---|
| Journal | Electronic Proceedings in Theoretical Computer Science, EPTCS |
| Volume | 354 |
| Pages (from-to) | 71-85 |
| Number of pages | 15 |
| ISSN | 2075-2180 |
| DOIs | |
| Publication status | Published - 8 Feb 2022 |
| Event | 10th International Workshop on Theorem Proving Components for Educational Software, ThEdu 2021 - Pittsburgh, United States Duration: 11 Jul 2021 → … |
Conference
| Conference | 10th International Workshop on Theorem Proving Components for Educational Software, ThEdu 2021 |
|---|---|
| Country/Territory | United States |
| City | Pittsburgh |
| Period | 11/07/2021 → … |
Citation Styles
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver