Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned
J{\o}rgen Villadsen (Technical University of Denmark)
TL;DR
MiniCalc is a web-based teaching tool for first-order logic that uses a minimal sequent calculus and integrates proof verification with Isabelle, aiming to improve logic education.
Contribution
The paper introduces MiniCalc, a minimal sequent calculus web app for teaching first-order logic, including lessons learned from its use in university education.
Findings
Effective in teaching first-order logic concepts.
Integration with Isabelle enhances proof verification.
Positive feedback from educational use.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.