Teaching Higher-Order Logic Using Isabelle
arXiv:2404.05458 · doi:10.4204/EPTCS.400.5
Abstract
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.
In Proceedings ThEdu'23, arXiv:2404.03709
References in corpus (7)
- Natural Deduction Assistant (NaDeA)
- Isabelle/HOL as a Meta-Language for Teaching Logic
- ANITA: Analytic Tableau Proof Assistant
- SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
- A Proof Tree Builder for Sequent Calculus and Hoare Logic
- On Exams with the Isabelle Proof Assistant
- Teaching Intuitionistic and Classical Propositional Logic Using Isabelle