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

arXiv: https://arxiv.org/abs/2505.05988 · HTML: https://mlsanity.com/paper/2505.05988/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 26 references that are in the map.
- First posted on arXiv 9 May 2025.

## Builds on (most cited first, 6 of 6)

- [SeCaV: A Sequent Calculus Verifier in Isabelle/HOL](https://mlsanity.com/paper/2204.03884/) (2022)
- [Natural Deduction Assistant (NaDeA)](https://mlsanity.com/paper/1904.00618/) (2019)
- [Isabelle/HOL as a Meta-Language for Teaching Logic](https://mlsanity.com/paper/2010.16014/) (2020)
- [The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs](https://mlsanity.com/paper/1803.01467/) (2018)
- [Carnap: An Open Framework for Formal Reasoning in the Browser](https://mlsanity.com/paper/1803.03092/) (2018)
- [A Mobile Application for Self-Guided Study of Formal Reasoning](https://mlsanity.com/paper/2002.12553/) (2020)

## Abstract (arXiv)

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.