Filter
Top Products
Preface
HOL Light is a relatively new version of the HOL theorem prover (Gordon and
Melham 1993). The whole implementation, even the axiomatization of the logic,
has been re-engineered and simplified. Compared with other versions of HOL, it is
relatively small and clean, and makes modest demands on the machine it is run on.
The material that follows is not only a tutorial on the use of HOL Light and its
interaction language, but also provides a detailed discussion of the implementation.
HOL Light proves theorems in a system of classical higher order logic based
on polymorphic simple type theory. All proof proceeds by the application of low-
level primitive rules, maintaining a high degree of reliability. However, a suite of
derived rules for proving various useful theorems automatically is provided, as is a
full programming language in which users can implement their own derived rules.
A number of useful mathematical theories, e.g. real analysis, are already available.
To become an expert user of HOL Light, it is necessary to know something
about programming in CAML Light, which is the implementation and interaction
language. However, for readers primarily interested in theorem proving, it’s no
doubt somewhat dispiriting to spend a long time studying functional programming
before even beginning to prove theorems. We have tried to minimize this problem
in the organization that follows.
We begin with a short introductory chapter highlighting the basic features of
CAML and HOL, including the basic mechanism of user interaction and the princi-
ples behind derived inference rules. Features of HOL and CAML are illustrated as
we go, and most readers will be able to pick up the general ideas. This introduction
is followed by the two larger Parts, comprising systematic introductions to CAML
and HOL respectively. While these can be tackled in sequence, the impatient reader
can read them in parallel, or even read the HOL part first and refer back to the
CAML part as needed. (Indeed, there are a number of obvious parallels between
CAML and the HOL logic, with both being an enriched version of lambda calculus,
and both having a similar system of types. Reading these parts in parallel will show
many similar concepts like currying and polymorphism in two different contexts.)
Since HOL Light is aimed particularly at the enthusiast who wants to implement
custom theorem-proving tools, a third Part gives an overview of the implementation,
explaining the basic structure of the system and discussing various design decisions.
We hope that users interested in building custom theorem proving tools, or just
in understanding the architecture of a modern theorem prover, will find something
of interest in HOL Light and the present document. While we are writing primarily
for those interested in theorem proving, the system might be considered interesting
for two other reasons: it is a large application of (impure) functional programming,
and it includes a systematic logical development of nontrivial mathematics from its
very foundations `a la Principia Mathematica (Whitehead and Russell 1910).
I do not assume that the reader is familiar with HOL or any similar system.
Some knowledge of programming and of basic logic would be of great benefit, but
not essential. However the present introduction is not comprehensive, and the
serious user will need to spend time browsing through the source code.
iii