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 Statements Referenced by

All labels observed (6)

Label Occurrences
Isabelle proof assistant canonical 5
Isabelle theorem prover 4
Isabelle/HOL 3

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 ⓘ
Markus Wenzel ⓘ
surface form: Makarius Wenzel

Technical University of Munich ⓘ
surface form: Technische Universität München

Tobias Nipkow ⓘ
Cambridge University ⓘ
surface form: University of Cambridge
hasCommunityResource Archive of Formal Proofs ⓘ
surface form: Archive of Formal Proofs (AFP)
hasComponent Code generator ⓘ
Document preparation system ⓘ
Isabelle/FOL ⓘ
Isabelle/HOL: A Proof Assistant for Higher-Order Logic ⓘ
surface form: Isabelle/HOL

Isabelle proof assistant self-linksurface differs ⓘ
surface form: Isabelle/Isar

Isabelle/ZF ⓘ
Isabelle/jEdit ⓘ
Nitpick ⓘ
Quickcheck ⓘ
Sledgehammer ⓘ
hasDocumentation Isabelle/HOL: A Proof Assistant for Higher-Order Logic ⓘ
surface form: Isabelle/HOL Tutorial

Isabelle/Isar Reference Manual ⓘ
hasRepository https://isabelle.in.tum.de ⓘ
initialReleaseYear 1986 ⓘ
license BSD license ⓘ
surface form: BSD-style license

open source ⓘ
namedAfter Isabelle proof assistant self-linksurface differs ⓘ
surface form: Isabelle (a generic logical framework)
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 ⓘ
surface form: Poly/ML (runtime)

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 proof assistant self-linksurface differs ⓘ
surface form: Isabelle/HOL

Zermelo–Fraenkel set theory ⓘ
surface form: Isabelle/ZF

first-order logic (via object logics) ⓘ
higher-order logic ⓘ
set theory (via HOL and other object logics) ⓘ
supportsStyle declarative proofs ⓘ
procedural proofs ⓘ
usesProofLanguage Isar ⓘ

Referenced by (15)

Full triples — surface form annotated when it differs from this entity's canonical label.

Tobias Nipkow → knownFor → Isabelle proof assistant ⓘ
LCF theorem prover → influenced → Isabelle proof assistant ⓘ
this entity surface form: Isabelle theorem prover
LCF theorem prover → relatedTo → Isabelle proof assistant ⓘ
this entity surface form: Isabelle/HOL
Isabelle proof assistant → supportsLogic → Isabelle proof assistant self-linksurface differs ⓘ
subject surface form: Isabelle
this entity surface form: Isabelle/HOL
Isabelle proof assistant → hasComponent → Isabelle proof assistant self-linksurface differs ⓘ
subject surface form: Isabelle
this entity surface form: Isabelle/Isar
Isabelle proof assistant → namedAfter → Isabelle proof assistant self-linksurface differs ⓘ
subject surface form: Isabelle
this entity surface form: Isabelle (a generic logical framework)
Isabelle/HOL: A Proof Assistant for Higher-Order Logic → focusesOn → Isabelle proof assistant ⓘ
Isabelle/HOL: A Proof Assistant for Higher-Order Logic → relatedTo → Isabelle proof assistant ⓘ
this entity surface form: Isabelle theorem prover
Types and Programming Languages (research contributions) → usesTool → Isabelle proof assistant ⓘ
this entity surface form: Isabelle theorem prover
Markus Wenzel → knownFor → Isabelle proof assistant ⓘ
Markus Wenzel → primaryDeveloperOf → Isabelle proof assistant ⓘ
Markus Wenzel → notablePublication → Isabelle proof assistant ⓘ
this entity surface form: Isar – A Generic Interpretative Approach to Readable Formal Proofs
Gerwin Klein → knownFor → Isabelle proof assistant ⓘ
this entity surface form: Isabelle/HOL
Gerwin Klein → uses → Isabelle proof assistant ⓘ
this entity surface form: Isabelle theorem prover
Vampire automated theorem prover → relatedTo → Isabelle proof assistant ⓘ