# Teaching Higher-Order Logic Using Isabelle

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 21 references that are in the map.
- First posted on arXiv 8 Apr 2024.

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

- [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)
- [Teaching Intuitionistic and Classical Propositional Logic Using Isabelle](https://mlsanity.com/paper/2202.03567/) (2022)
- [Computational Logic: Its Origins and Applications](https://mlsanity.com/paper/1712.04375/) (2017)
- [Learning how to Prove: From the Coq Proof Assistant to Textbook Style](https://mlsanity.com/paper/1803.01466/) (2018)
- [Natural Deduction and the Isabelle Proof Assistant](https://mlsanity.com/paper/1803.01473/) (2018)
- [ANITA: Analytic Tableau Proof Assistant](https://mlsanity.com/paper/2303.05864/) (2023)
- [A Proof Tree Builder for Sequent Calculus and Hoare Logic](https://mlsanity.com/paper/2303.05865/) (2023)
- [On Exams with the Isabelle Proof Assistant](https://mlsanity.com/paper/2303.05866/) (2023)

## Abstract (arXiv)

We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier automation. To showcase our development and approach we explain a sample proof, describe the axioms and rules of our higher-order logic, and discuss our experience with teaching the subject in a classroom setting.