HOL (Higher Order Logic) denotes a family of
interactive theorem proving systems using similar
(higher-order) logics and implementation strategies. Systems in this family follow the
LCF approach as they are implemented as a library which defines an
abstract data type
In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a ''user'', of the data, specifically in terms of possible values, pos ...
of proven
theorem
In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of th ...
s such that new objects of this type can only be created using the functions in the library which correspond to
inference rule
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
s in
higher-order logic
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
. 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.
Systems in the HOL family use
ML 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".
Underlying logic
HOL systems use variants of
classical higher-order logic
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
, which has simple axiomatic foundations with few axioms and well-understood semantics.
The logic used in HOL provers is closely related to Isabelle/HOL, the most widely used logic of
Isabelle.
HOL implementations
Although HOL is a predecessor of Isabelle, various HOL derivatives remain active and in use. These are the four current HOL systems (sharing essentially the same logic):
# HOL4 the only presently maintained and developed system stemming from the HOL88 system, which was the culmination of the original HOL implementation effort, led by
Mike Gordon
Michael Eliot Gordon (born June 3, 1965) is an American bass guitarist and vocalist most recognized as a founding member of the band Phish. In addition to bass, Gordon is an accomplished banjo player, and is proficient at piano and guitar. He ...
. HOL88 included its own
ML implementation, which was in turn implemented on top of
Common Lisp
Common Lisp (CL) is a dialect of the Lisp programming language, published in ANSI standard document ''ANSI INCITS 226-1994 (S20018)'' (formerly ''X3.226-1994 (R1999)''). The Common Lisp HyperSpec, a hyperlinked HTML version, has been derived fro ...
. The systems that followed HOL88 (HOL90, hol98 and HOL4) were all implemented in
Standard ML
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of the ...
; while hol98 is
coupled
''Coupled'' is an American dating game show that aired on Fox from May 17 to August 2, 2016. It was hosted by television personality, Terrence J and created by Mark Burnett, of '' Survivor'', ''The Apprentice'', '' Are You Smarter Than a 5th G ...
to
Moscow ML
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of the ...
, HOL4 can be built with either Moscow ML or
Poly/ML. All come with large libraries of theorem proving code which implement extra automation on top of the very simple core code. HOL4 is BSD licensed.
#
HOL Light HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is aut ...
an experimental "minimalist" version of HOL which has since grown into another mainstream HOL variant; its logical foundations remain unusually simple. HOL Light, originally implemented in
Caml Light
Caml (originally an acronym for Categorical Abstract Machine Language) is a multi-paradigm, general-purpose programming language which is a dialect of the ML programming language family. Caml was developed in France at INRIA and ENS.
Caml is ...
, now uses
OCaml
OCaml ( , formerly Objective Caml) is a general-purpose programming language, general-purpose, multi-paradigm programming language which extends the Caml dialect of ML (programming language), ML with object-oriented programming, object-oriented ...
. HOL Light is available under the new BSD license.
ProofPower a collection of tools designed to provide special support for working with the
Z notation
The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.
History
In 1974, Jean-Raymond Abrial ...
for formal specification. 5 of the 6 tools are GNU GPL v2 licensed. The sixth (PPDaz) has a proprietary license.
HOL Zero a minimalist implementation focused on trustworthiness. HOL Zero is GNU GPL 3+ licensed.
Formal proof developments
The
CakeML project developed a formally proven compiler for ML. Previously, HOL was used to develop a formally proven
Lisp
A lisp is a speech impairment in which a person misarticulates sibilants (, , , , , , , ). These misarticulations often result in unclear speech.
Types
* A frontal lisp occurs when the tongue is placed anterior to the target. Interdental lisping ...
implementation running on ARM, x86 and PowerPC.
HOL was also used to formalize the
semantics
Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy
Philosophy (f ...
of x86 multiprocessors as well as the
machine code
In computer programming, machine code is any low-level programming language, consisting of machine language instructions, which are used to control a computer's central processing unit (CPU). Each instruction causes the CPU to perform a very ...
for
Power ISA
Power ISA is a reduced instruction set computer (RISC) instruction set architecture (ISA) currently developed by the OpenPOWER Foundation, led by IBM. It was originally developed by IBM and the now-defunct Power.org industry group. Power IS ...
and
ARM
In human anatomy, the arm refers to the upper limb in common usage, although academically the term specifically means the upper arm between the glenohumeral joint (shoulder joint) and the elbow joint. The distal part of the upper limb between th ...
architectures.
References
Further reading
* {{cite web
, last = Gordon
, first = Michael J. C.
, author-link = Michael J. C. Gordon
, year = 1996
, title = From LCF to HOL: A Short History
, url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html
, access-date = 2007-10-11
External links
HOL4 Project homepageThe HOL4 Description manual which includes a specification of the system's logic.
Virtual library formal methods information
Proof assistants
Logic in computer science
Software using the BSD license