arXiv:2505.05988v1 类别: cross 摘要: MiniCalc 是一个基于最小 sequent calculus 的网络应用，用于教授一阶逻辑。作为选项，证明可以在 Isabelle 证明助手中标记验证。我们介绍了近年来在我们大学使用该工具时学到的经验。