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

Observed surface forms (2)

Surface form	Occurrences
HOL theorem provers	2
HOL theorem prover family	1

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 ⓘ

Referenced by (5)

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

LCF theorem prover → conceptualBasisFor → HOL theorem prover ⓘ

this entity surface form: HOL theorem prover family

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

LCF theorem prover → influenced → HOL theorem prover ⓘ

this entity surface form: HOL theorem provers

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

this entity surface form: HOL theorem provers

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