用极简演绎逻辑教学工具，让初学者轻松掌握一阶逻辑推理。

Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned

• 基于极简序列演算设计教学工具
• 支持在Isabelle中验证证明过程
• 适用于高校逻辑课程教学实践

MiniCalc 是一个基于极简序列演算的网页教学应用，用于教授一阶逻辑。用户可选择在 Isabelle 证明助手内验证所构建的证明。本文总结了近年来在本校使用该工具的教学经验与收获。

原文摘要 · Abstract (English)

MiniCalc is a web app for teaching first-order logic based on a minimal sequent calculus. As an option the proofs can be verified in the Isabelle proof assistant. We present the lessons learned using the tool in recent years at our university.

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。