Teaching Higher-Order Logic Using Isabelle

Simon Tobias Lund, Jørgen Villadsen
4/8/2024
cs.LOcs.AI

No confident code implementation found for this paper.

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Subtyping in DHOL -- Extended preprint

78% match2025

Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality

77% match2026

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

77% match2025

Relating Answer Set Programming and Many-sorted Logics for Formal Verification

77% match2025

Lean-STaR: Learning to Interleave Thinking and Proving

77% match2024

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

76% match1 repo272025

Cite this paper

@article{lund2024teaching,
  title  = {Teaching Higher-Order Logic Using Isabelle},
  author = {Simon Tobias Lund and Jørgen Villadsen},
  year   = {2024},
  eprint = {2404.05458},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2404.05458v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2404.05458.svg)](https://codeofpaper.com/paper/2404.05458)

Discussion