# SeCaV: A Sequent Calculus Verifier in Isabelle/HOL

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Apr 2022.

## Built on by (most cited first, 4 of 4)

- [Theory-Scale Auto-Formalization of Logics for Computer Science](https://mlsanity.com/paper/2606.26525/) (2026)
- [On Exams with the Isabelle Proof Assistant](https://mlsanity.com/paper/2303.05866/) (2023)
- [Teaching Higher-Order Logic Using Isabelle](https://mlsanity.com/paper/2404.05458/) (2024)
- [Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned](https://mlsanity.com/paper/2505.05988/) (2025)

## Abstract (arXiv)

We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into the full SeCaV syntax. We leverage the power of Isabelle/HOL as a proof checker for our SeCaV derivations. The interactive features of Isabelle/HOL make our system transparent. For instance, the user can simply click on a side condition to see its exact definition. Our formalized soundness and completeness proofs pertain exactly to the calculus as exposed to the user and not just to some model of our tool. Users can also write their derivations in the SeCaV Unshortener, which provides a lighter syntax, and expand them for later verification. We have used both tools in our teaching.