Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned
arXiv:2505.05988 · doi:10.4204/EPTCS.419.5
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.
arXiv commentIn Proceedings ThEdu24, arXiv:2505.04677
References in corpus (7)
- Kripke Models for Classical Logic
- Natural Deduction Assistant (NaDeA)
- The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
- Isabelle/HOL as a Meta-Language for Teaching Logic
- Carnap: An Open Framework for Formal Reasoning in the Browser
- SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
- A Mobile Application for Self-Guided Study of Formal Reasoning