Statements (22)
| Predicate | Object |
|---|---|
| gptkbp:instanceOf |
gptkb:software
gptkb:theorem_prover |
| gptkbp:basedOn |
higher-order logic
|
| gptkbp:citation |
gptkb:Gordon,_M._J._C.,_&_Melham,_T._F._(1993)._Introduction_to_HOL:_A_theorem_proving_environment_for_higher_order_logic.
Gordon, M. J. C., Milner, R., & Wadsworth, C. P. (1979). Edinburgh LCF. |
| gptkbp:developedBy |
gptkb:Mike_Gordon
|
| gptkbp:firstReleased |
1986
|
| gptkbp:influenced |
gptkb:HOL4
gptkb:HOL_Light gptkb:ProofPower gptkb:Isabelle |
| gptkbp:license |
open source
|
| gptkbp:notableFor |
verification of ARM6 processor
verification of floating-point hardware |
| gptkbp:operatingSystem |
cross-platform
|
| gptkbp:programmingLanguage |
ML
|
| gptkbp:usedFor |
gptkb:mathematics
formal verification |
| gptkbp:website |
https://hol-theorem-prover.org/
|
| gptkbp:bfsParent |
gptkb:LCF_theorem_prover
|
| gptkbp:bfsLayer |
6
|
| https://www.w3.org/2000/01/rdf-schema#label |
HOL theorem prover
|