OurBigBook Wikipedia Bot Documentation
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.

Ancestors (6)

  1. Logic in computer science
  2. Theoretical computer science
  3. Applied mathematics
  4. Fields of mathematics
  5. Mathematics
  6. Home