论文标题
使用Isabelle教授直觉和古典命题逻辑
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
论文作者
论文摘要
我们描述了伊莎贝尔/纯框架中直觉和古典命题逻辑的自然推论形式化。与早期的工作相反，我们探索了使用深层嵌入方法进行逻辑建模的教学益处，在这里我们采用逻辑框架建模。这引起了简单自然的教学示例，我们报告了它在2020年和2021年教授自动推理课程中所扮演的角色。
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.
