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

LogiKEy 方法论以经典高阶逻辑（HOL）为通用元逻辑，通过语义嵌入在单一证明助手（如 Isabelle/HOL）中统一编码多种对象逻辑。该方法已用于计算机科学、数学及哲学混合课程逾十年，通过从命题逻辑到模态逻辑、动态认识论逻辑及义务逻辑的分级示例，帮助学生实验与比较不同逻辑系统。