\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Isabelle

Table of Contents

1. Introduction

Isabelle is a metalogical logical framework (but Isabelle/HOL is a metalogical framework, which is a logical framework that allows us to prove results about deductive systems; this is because HOL is a metalogical framework). Recall, logical frameworks reason within deductive systems. Isabelle is a bit like a tool to create proof assistants, which is why we often see things like Isabelle/X for various choices of X.

2. References

2.1. Early Papers

  • Lawrence Paulson,
    "The Foundation of a Generic Theorem Prover".
    arXiv:cs/9301105, 37 pages.
    • Introduces Isabelle/Pure as a fragment of intuitionistic higher-order logic.
  • Lawrence Paulson,
    "Isabelle: The Next 700 Theorem Provers".
    arXiv:cs/9301106
  • Lawrence Paulson,
    "Natural Deduction as Higher-Order Resolution".
    arXiv:cs/9301104

2.2. Set Theory in Isabelle

  • Florian Rabe and Mihnea Iancu,
    "A Formalized Set-Theoretical Semantics of Isabelle/HOL".
    PDF, 20 pages
  • Bohua Zhan,
    "Formalization of the fundamental group in untyped set theory using auto2".
    arXiv:1707.04757, 17 pages.
    • One of the few formalizations using both untyped set theory and Isabelle

Last Updated 2022-02-22 Tue 08:31.