Isabelle/ML | GPTKB 2.0

All labels observed (3)

Label	Occurrences
Isabelle/ML canonical	2
Isabelle/ML back-end	1
Isabelle/ML runtime environment	1

How this entity was disambiguated

This entity first appeared as the object of triple T9810247 — 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/ML
Context triple: [Markus Wenzel, notableWork, Isabelle/ML]

A. Isabelle 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.
B. Isabelle/HOL: A Proof Assistant for Higher-Order Logic
"Isabelle/HOL: A Proof Assistant for Higher-Order Logic" is a foundational book and system documentation that presents the Isabelle/HOL interactive theorem prover, widely used for formal verification and higher-order logic reasoning in computer science and mathematics.
C. Boyer–Moore theorem prover
The Boyer–Moore theorem prover is an influential automated reasoning system for first-order logic and recursive function theory, notable for pioneering techniques in mechanical proof and program verification.
D. 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.
E. Satisfiability Modulo Theories (SMT)
Satisfiability Modulo Theories (SMT) is a framework in computer science and mathematical logic for deciding the satisfiability of logical formulas with respect to background theories such as arithmetic, bit-vectors, arrays, and data types, widely used in verification, synthesis, and automated reasoning.
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/ML
Target entity description: Isabelle/ML is the ML-based implementation and extension language used to develop and script the Isabelle interactive theorem prover.

A. Isabelle 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.
B. Isabelle/HOL: A Proof Assistant for Higher-Order Logic
"Isabelle/HOL: A Proof Assistant for Higher-Order Logic" is a foundational book and system documentation that presents the Isabelle/HOL interactive theorem prover, widely used for formal verification and higher-order logic reasoning in computer science and mathematics.
C. Boyer–Moore theorem prover
The Boyer–Moore theorem prover is an influential automated reasoning system for first-order logic and recursive function theory, notable for pioneering techniques in mechanical proof and program verification.
D. 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.
E. Satisfiability Modulo Theories (SMT)
Satisfiability Modulo Theories (SMT) is a framework in computer science and mathematical logic for deciding the satisfiability of logical formulas with respect to background theories such as arithmetic, bit-vectors, arrays, and data types, widely used in verification, synthesis, and automated reasoning.
F. None of above. chosen

Statements (50)

Predicate	Object
instanceOf	extension language ⓘ implementation language ⓘ programming language ⓘ
basedOn	Standard ML ⓘ
category	domain-specific extension of Standard ML ⓘ theorem prover implementation language ⓘ
designedFor	tight integration with the Isabelle logical environment ⓘ
documentedIn	Isabelle/Isar Implementation manual ⓘ linked to: Isabelle/Isar Reference Manual
executedIn	Isabelle/ML runtime environment ⓘ linked to: Isabelle/ML JVM-based Isabelle process in recent Isabelle versions ⓘ
extends	Standard ML with Isabelle-specific libraries ⓘ Standard ML with Isabelle-specific syntax support ⓘ Standard ML with logical infrastructure access ⓘ
hasFeature	access to Isabelle context data ⓘ antiquotations for embedding ML in Isar ⓘ exception handling ⓘ higher-order functions ⓘ interfaces to external tools via Isabelle infrastructure ⓘ module system from Standard ML ⓘ parallel and asynchronous programming support via Isabelle runtime ⓘ pattern matching ⓘ quasi-quotations for logical entities ⓘ static type system ⓘ tailored libraries for terms and types ⓘ
integratedWith	Isabelle code generator infrastructure ⓘ Isabelle proof context ⓘ Isabelle term representation ⓘ Isabelle theory context ⓘ Isabelle type system ⓘ Isabelle/Isar ⓘ linked to: Isar proof language
maintainedBy	Isabelle development team ⓘ
primaryAuthor	Makarius Wenzel ⓘ linked to: Markus Wenzel
provides	APIs for defining new attributes ⓘ APIs for defining new commands ⓘ APIs for defining new proof methods ⓘ APIs for manipulating Isabelle terms ⓘ APIs for manipulating Isabelle theories ⓘ APIs for manipulating Isabelle types ⓘ APIs for manipulating proof states ⓘ
usedBy	Isabelle tool developers ⓘ advanced Isabelle users ⓘ
usedFor	developing the Isabelle theorem prover ⓘ extending the Isabelle system ⓘ implementing Isabelle attributes ⓘ implementing Isabelle methods ⓘ implementing Isabelle proof tools ⓘ implementing Isabelle tactics ⓘ implementing proof procedures in Isabelle ⓘ scripting Isabelle tools ⓘ
usedIn	Isabelle ⓘ

How these facts were elicited

Referenced by (4)

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

Markus Wenzel → notableWork → Isabelle/ML ⓘ

Isabelle/jEdit → uses → Isabelle/ML back-end ⓘ

linked to: Isabelle/ML

Quickcheck → implementedIn → Isabelle/ML ⓘ

Isabelle/ML → executedIn → Isabelle/ML runtime environment ⓘ