Source: wikibot/hol-proof-assistant
= HOL (proof assistant)
{wiki=HOL_(proof_assistant)}
HOL (Higher-Order Logic) is a family of proof assistants that are based on the higher-order logic formalism. One of the most prominent members of this family is HOL4, but there are also others, like HOL Light and Isabelle/HOL, which share similar principles but may differ in implementation and features.