World Library  
Flag as Inappropriate
Email this Article

HOL theorem prover

Article Id: WHEBN0013675921
Reproduction Date:

Title: HOL theorem prover  
Author: World Heritage Encyclopedia
Language: English
Subject: Isabelle (proof assistant), Formal verification, Logic in computer science, Proof assistant, Twelf, Michael J. C. Gordon
Publisher: World Heritage Encyclopedia

HOL theorem prover

HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharing similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language. This library implements an abstract data type of proven theorems so that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. In this way, a large system can be built on top of a small trusted kernel.

Systems in the HOL family use the ML programming language or its successors. ML was originally developed along with LCF to serve the purpose of a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language".


There are four HOL systems (sharing essentially the same logic) that are still maintained and developed.

  • The first, HOL4 stems from the HOL88 system, which was the culmination of the original HOL implementation effort, led by Mike Gordon. HOL88 included its own ML implementation, which was in turn implemented on top of Common Lisp. The implementations following HOL88 (HOL90, hol98 and HOL4) all used Standard ML as the implementation language. The hol98 system is tied to the Moscow ML implementation of Standard ML; HOL4 can be built with either Moscow ML or Poly/ML. Of these four systems, only HOL4 is being maintained and developed. All come with large libraries of theorem proving code. These implement extra automation on top of the very simple core code. HOL4 is BSD licensed.[1]
  • The second current implementation is HOL Light. This started as an experimental "minimalist" version of HOL. Although it has subsequently grown into another mainstream HOL variant, its logical foundations remain unusually simple. HOL Light used to be implemented in Caml Light, but now uses OCaml. HOL Light is available under the new BSD license.[2]
  • The third current implementation is
  • The fourth is

HOL is a predecessor of Isabelle.


External links

  • HOL4 Project homepage
  • Documents specifying HOL's basic logic
  • The HOL4 Description manual, which includes a specification of the system's logic.
  • Virtual library formal methods information

This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from Hawaii eBook Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.