HOL theorem prover

E807591

higher-order logic theorem prover interactive theorem prover proof assistant

The HOL theorem prover is an interactive proof assistant for higher-order logic, widely used in formal verification of hardware, software, and mathematical theories.

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

All labels observed (3)

Label	Occurrences
HOL theorem prover canonical	2
HOL theorem provers	2
HOL theorem prover family	1

How this entity was disambiguated

This entity first appeared as the object of triple T9566623 — 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: HOL theorem prover
Context triple: [Arthur John Robin Gorell Milner, notableWork, HOL theorem prover]

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. 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.
C. 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.
D. 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.
E. ACL2 theorem proving system
The ACL2 theorem proving system is an automated reasoning tool and programming language based on a subset of Common Lisp, widely used for modeling and mechanically verifying hardware, software, and mathematical theorems.
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: HOL theorem prover
Target entity description: The HOL theorem prover is an interactive proof assistant for higher-order logic, widely used in formal verification of hardware, software, and mathematical theories.

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. 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.
C. 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.
D. 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.
E. ACL2 theorem proving system
The ACL2 theorem proving system is an automated reasoning tool and programming language based on a subset of Common Lisp, widely used for modeling and mechanically verifying hardware, software, and mathematical theorems.
F. None of above. chosen

Statements (45)

Predicate	Object
instanceOf	higher-order logic theorem prover ⓘ interactive theorem prover ⓘ proof assistant ⓘ
basedOn	classical higher-order logic ⓘ
belongsTo	HOL family of theorem provers NERFINISHED ⓘ
developedAt	University of Cambridge NERFINISHED ⓘ
developedFrom	LCF theorem prover NERFINISHED ⓘ
hasApplicationDomain	floating-point hardware verification ⓘ microprocessor verification ⓘ protocol verification ⓘ security-critical software verification ⓘ
hasConcept	derived inference rules ⓘ tactics and tacticals ⓘ theory hierarchy ⓘ
hasFeature	LCF-style architecture ⓘ ML programming interface ⓘ interactive proof development ⓘ small trusted kernel ⓘ tactic-based proof construction ⓘ
hasGoal	increasing assurance in critical systems ⓘ
hasProperty	extensible via ML programming ⓘ soundness guaranteed by small kernel ⓘ
implementedIn	ML ⓘ
influenced	HOL Light NERFINISHED ⓘ HOL family of theorem provers NERFINISHED ⓘ HOL4 NERFINISHED ⓘ Isabelle/HOL NERFINISHED ⓘ ProofPower-HOL NERFINISHED ⓘ
relatedTo	ACL2 NERFINISHED ⓘ Coq NERFINISHED ⓘ Isabelle NERFINISHED ⓘ PVS NERFINISHED ⓘ
supports	datatype definition ⓘ higher-order logic ⓘ inductive definitions ⓘ mechanized proof checking ⓘ proof automation via tactics ⓘ theory definition ⓘ
usedBy	formal methods researchers ⓘ hardware verification engineers ⓘ software verification engineers ⓘ
usedFor	formal verification ⓘ formalization of mathematics ⓘ hardware verification ⓘ software verification ⓘ

How these facts were elicited

Referenced by (5)

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

Arthur John Robin Gorell Milner → notableWork → HOL theorem prover ⓘ

Arthur John Robin Gorell Milner → developed → HOL theorem prover ⓘ

LCF theorem prover → influenced → HOL theorem prover ⓘ

this entity surface form: HOL theorem provers

LCF theorem prover → conceptualBasisFor → HOL theorem prover ⓘ

this entity surface form: HOL theorem prover family

The Definition of Standard ML → influenced → HOL theorem prover ⓘ