LogiKEy 方法论：用数学证明助手教授逻辑学

LogiKEy 方法论以经典高阶逻辑（HOL）作为通用元逻辑，通过语义嵌入将经典与非经典对象逻辑编码其中，使 Isabelle/HOL 等单一证明助手及其自动定理证明器和（反）模型查找器成为统一教学环境。该方法已用于计算机科学、数学和哲学混合学生群体的课程、暑期学校与教程超过十年。