HOL (proof assistant)

<p>HOL (Higher Order Logic) denotes a family of <a href="/facts/Proof_assistant/hjFGxLPn">interactive theorem proving systems</a> using similar <a href="/facts/Higher-order_logic/hdUhry6m">(higher-order)</a> logics and implementation strategies. Systems in this family follow the <a href="/facts/LCF_(theorem_prover)/wJsqr2rJ">LCF</a> approach as they are implemented as a library which defines an <a href="/facts/Abstract_data_type/BaVGSHNP">abstract data type</a> of proven <a href="/facts/Theorem/f2Pe1FMD">theorems</a> such that new objects of this type can only be created using the functions in the library which correspond to <a href="/facts/Inference_rule/QV5NklQ9">inference rules</a> in <a href="/facts/Higher-order_logic/hdUhry6m">higher-order logic</a>. As long as these functions are correctly implemented, all theorems proven in the system must be valid. As such, a large system can be built on top of a small trusted kernel.
</p><p>Systems in the HOL family use <a href="/facts/ML_(programming_language)/RfwxASRF">ML</a> or its successors. ML was originally developed along with LCF as a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language".
</p>

HOL (proof assistant) open-in-new

HOL (proof assistant)