The
Isabelle theorem prover is an
interactive theorem prover, a
Higher Order Logic (HOL) theorem prover. It is an
LCF-style theorem prover (written in
Standard ML), so it is based on a small logical core to ease logical correctness. Isabelle is generic: it provides a meta-logic (a weak
type theory), which is used to encode object logics like
First-order logic (FOL),
Higher-order logic (HOL) or
Zermelo–Fraenkel set theory (ZFC). Isabelle's main proof method is a
higher-order version of
resolution, based on higher-order
unification. Though interactive, Isabelle also features efficient automatic reasoning tools, such as a
term rewriting engine and a
tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like
Gödel's completeness theorem, Gödel's theorem about the consistency of the
axiom of choice, the
prime number theorem, correctness of
security protocols, and properties of
programming language semantics. The Isabelle theorem prover is
free software, released under the revised
BSD license.