Filter
Top Products
Chapter 1
Introduction
In the following chapter we explain the key ideas behind HOL Light and cover the
basics of interaction with the system. It is intended merely to give a brief taste,
and readers wanting a more systematic introduction should study the subsequent
chapters.
1.1 What is HOL Light?
There are many computer programs, e.g. as used in ordinary pocket calculators,
for dealing with numerical problems like adding 2 and 2. Other programs, such as
the computer algebra systems Maple
1
and Mathematica
2
, can cope not just with
particular numbers, but also with expressions involving variables. For example they
can calculate that the derivative of x
2
with respect to x evaluated at the point x is
2x.
These programs are usually thought of as calculating the answers to problems.
But one can also look at them as systems that produce, on demand, mathematical
theorems in a certain class. If we use the symbol to indicate that an assertion is
actually a true theorem of mathematics, we might say that these programs produce
the following theorems, when given the appropriate left-hand sides:
2 + 2 = 4
or
d
dx
x
2
= 2x
HOL Light is similar: it is a system for producing theorems on demand. Com-
pared with calculators or computer algebra systems (CASs), it has two great ad-
vantages:
• HOL Light can produce theorems covering a wide mathematical range, e.g.
involving infinite sets and so-called quantifiers like ‘there exists some integer
such that . . .’ or ‘for any set of real numbers .. .’. By contrast, calculators and
CASs mainly produce unconditional equations with any variables implicitly
regarded as universal.
• The theorems it produces can be relied on to be unambiguous in meaning and
rigorously proven. By contrast, the exact readings of ‘theorems’ produced by
1
Maple is a registered trademark of Waterloo Maple Software.
2
Mathematica is a registered trademark of Wolfram Research Inc.
1