Filter
Top Products
6 CHAPTER 1. INTRODUCTION
depending on the input. It corresponds naturally to what a logician would think of
as a ‘derived rule’.
CAML Light, described in the next Part, is a full programming language, so
one can perform essentially any kinds of inference one wants, provided it is reduced
to the existing infrastructure of primitive and derived rules. Derived rules often
have a recursive structure, passing over the input term and transforming it into an
appropriate theorem. They may also do different things depending, for example, on
the logical structure of the input, the names of variables, and so on. All this will
be illustrated in more detail in what follows.
Further reading
The original textbook on Edinburgh LCF by Gordon, Milner, and Wadsworth (1979)
introduces many of the basic ideas in HOL Light; see also the later book by Paul-
son (1987) on a re-engineered version ‘Cambridge LCF’. The general approach to
theorem-proving described above is, as emphasized by Gordon (1982), largely in-
dependent of the particular logic one works with, e.g. the original LCF (logic of
computable functions), higher order logic, or first order set theory. The original
HOL was born when Gordon used the Cambridge LCF system to implement clas-
sical higher order logic. There is a book by Gordon and Melham (1993) describing
an early version of the system ‘HOL88’, while an interesting historical survey of
the development of LCF and HOL is given by Gordon (2000). The original ML is
also described in the early LCF publications. CAML Light has extensive on-line
documentation and a book (in French) by Weis and Leroy (1993) devoted to it.
Another ML version, Standard ML, is described by Paulson (1991).