Isabelle proof assistant

E238245

formal methods tool higher-order logic theorem prover interactive theorem prover proof assistant

Isabelle proof assistant is a widely used interactive theorem prover and generic proof assistant designed for formal verification and mathematical logic, particularly known for its support of higher-order logic.

Try in SPARQL Jump to: Surface forms Disambiguation Statements Elicitation Referenced by

All labels observed (9)

Label	Occurrences
Isabelle proof assistant canonical	13
Isabelle/HOL	8
Isabelle theorem prover	5
Isabelle interactive theorem prover	2
Isabelle (a generic logical framework)	1
Isabelle/HOL testing framework research	1
Isabelle/HOL theories	1
Isabelle/Isar	1
Isar – A Generic Interpretative Approach to Readable Formal Proofs	1

How this entity was disambiguated

This entity first appeared as the object of triple T2139663 — resolving that mention is where its identity was fixed. The disambiguator weighed these candidate entities and picked the highlighted one (or “None”, minting a new entity). This is how homonymy is resolved: the same surface form can point to different entities.

NED1 Entity disambiguation (via context triple) gpt-5-mini-2025-08-07

Target entity: Isabelle proof assistant
Context triple: [Tobias Nipkow, knownFor, Isabelle proof assistant]

A. LCF theorem prover
The LCF theorem prover is an early interactive proof system that pioneered the use of higher-order logic and the LCF-style architecture, forming the conceptual basis for later provers like HOL and Isabelle.
B. Hoare logic
Hoare logic is a formal system in computer science used to reason rigorously about the correctness of computer programs using logical assertions about program states.
C. Knuth–Bendix completion algorithm
The Knuth–Bendix completion algorithm is a procedure in term rewriting and automated theorem proving that transforms a set of equations into a confluent rewriting system, enabling decision of word problems in algebraic structures.
D. Hindley–Milner type system
The Hindley–Milner type system is a classical polymorphic type system used in many functional programming languages, notable for enabling type inference without explicit type annotations.
E. Gilles Dowek
Gilles Dowek is a French logician and computer scientist known for his influential work in proof theory, type systems, and automated deduction.
F. None of above. chosen
G. Unsure - the case is ambiguous/there is not enough information to decide.

NED2 Entity disambiguation (via description) gpt-5-mini-2025-08-07

Target entity: Isabelle proof assistant
Target entity description: Isabelle proof assistant is a widely used interactive theorem prover and generic proof assistant designed for formal verification and mathematical logic, particularly known for its support of higher-order logic.

A. LCF theorem prover
The LCF theorem prover is an early interactive proof system that pioneered the use of higher-order logic and the LCF-style architecture, forming the conceptual basis for later provers like HOL and Isabelle.
B. Hoare logic
Hoare logic is a formal system in computer science used to reason rigorously about the correctness of computer programs using logical assertions about program states.
C. Knuth–Bendix completion algorithm
The Knuth–Bendix completion algorithm is a procedure in term rewriting and automated theorem proving that transforms a set of equations into a confluent rewriting system, enabling decision of word problems in algebraic structures.
D. Hindley–Milner type system
The Hindley–Milner type system is a classical polymorphic type system used in many functional programming languages, notable for enabling type inference without explicit type annotations.
E. Gilles Dowek
Gilles Dowek is a French logician and computer scientist known for his influential work in proof theory, type systems, and automated deduction.
F. None of above. chosen

Statements (62)

Predicate	Object
instanceOf	formal methods tool ⓘ higher-order logic theorem prover ⓘ interactive theorem prover ⓘ proof assistant ⓘ
applicationDomain	formal verification of hardware ⓘ formal verification of software ⓘ formalization of mathematics ⓘ
category	formal verification tool ⓘ theorem proving software ⓘ
developer	Lawrence C. Paulson ⓘ Makarius Wenzel ⓘ linked to: Markus Wenzel Technische Universität München ⓘ linked to: Technical University of Munich Tobias Nipkow ⓘ University of Cambridge ⓘ linked to: Cambridge University
hasCommunityResource	Archive of Formal Proofs (AFP) ⓘ linked to: Archive of Formal Proofs
hasComponent	Code generator ⓘ Document preparation system ⓘ Isabelle/FOL ⓘ Isabelle/HOL ⓘ linked to: Isabelle/HOL: A Proof Assistant for Higher-Order Logic Isabelle/Isar ⓘ linked to: Isabelle proof assistant Isabelle/ZF ⓘ Isabelle/jEdit ⓘ Nitpick ⓘ Quickcheck ⓘ Sledgehammer ⓘ
hasDocumentation	Isabelle/HOL Tutorial ⓘ linked to: Isabelle/HOL: A Proof Assistant for Higher-Order Logic Isabelle/Isar Reference Manual ⓘ
hasRepository	https://isabelle.in.tum.de ⓘ
initialReleaseYear	1986 ⓘ
license	BSD-style license ⓘ linked to: BSD license open source ⓘ
namedAfter	Isabelle (a generic logical framework) ⓘ linked to: Isabelle proof assistant
notableUse	Archive of Formal Proofs ⓘ CompCert-related formalisations (via HOL) and C semantics work ⓘ seL4 microkernel verification ⓘ
operatingSystem	Linux ⓘ Windows ⓘ macOS ⓘ
primaryInterface	Isabelle/jEdit ⓘ Isar proof language ⓘ
programmingLanguage	Poly/ML (runtime) ⓘ linked to: Poly/ML Scala ⓘ Standard ML ⓘ
supportsFeature	automated proof search ⓘ code generation to functional languages ⓘ coinductive definitions ⓘ document generation (LaTeX, PDF) ⓘ inductive definitions ⓘ integration with external automated theorem provers ⓘ interactive proof development ⓘ locales and type classes ⓘ polymorphic types ⓘ type inference ⓘ
supportsLogic	Isabelle/FOL ⓘ Isabelle/HOL ⓘ linked to: Isabelle proof assistant Isabelle/ZF ⓘ linked to: Zermelo–Fraenkel set theory first-order logic (via object logics) ⓘ higher-order logic ⓘ set theory (via HOL and other object logics) ⓘ
supportsStyle	declarative proofs ⓘ procedural proofs ⓘ
usesProofLanguage	Isar ⓘ

How these facts were elicited