|
|
The History of the HOL System
(Based on the preface to the HOL system
Description.)
The HOL System is designed to support interactive
theorem proving in higher order logic (hence the acronym `HOL'). To this end,
the formal logic is interfaced to a general purpose programming language (ML,
for meta-language) in which terms and theorems of the logic can be denoted,
proof strategies expressed and applied, and logical theories developed.
The version of higher order logic used in HOL is predicate calculus with terms
from the typed lambda calculus (i.e. simple type theory). This was originally
developed as a foundation for mathematics [1]. The
primary application area of HOL was initially intended to be the specification
and verification of hardware designs. (The use of higher order logic for this
purpose was first advocated by
Keith
Hanna [2].) However, the logic does not restrict
applications to hardware; HOL has been applied to many other areas.
The approach to mechanizing formal proof used in HOL is due to Robin Milner
[3], who also headed the team that designed and
implemented the language ML. That work centred on a system called LCF (logic
for computable functions), which was intended for interactive automated
reasoning about higher order recursively defined functions. The interface of
the logic to the meta-language was made explicit, using the type structure of
ML, with the intention that other logics eventually be tried in place of the
original logic. The HOL system is a direct descendant of LCF; this is
reflected in everything from its structure and outlook to its incorporation of
ML, and even to parts of its implementation. Thus HOL satisfies the early plan
to apply the LCF methodology to other logics.
The original LCF was implemented at Edinburgh in the early 1970's, and is now
referred to as `Edinburgh LCF'. Its code was ported from Stanford Lisp to
Franz Lisp by Gérard Huet at
INRIA, and was used in a
French research project called `Formel'. Huet's Franz
Lisp version of LCF was further developed at Cambridge by
Larry Paulson, and became
known as `Cambridge LCF'. The HOL system is implemented on top of an early
version of Cambridge LCF and consequently many features of both Edinburgh and
Cambridge LCF were inherited by HOL. For example, the axiomatization of higher
order logic used is not the classical one due to Church, but an equivalent
formulation influenced by LCF.
The language ML has now achieved status as a programming language in its own
right, although it was originally designed as the proof management language
for LCF. It is a functional language distinguished particularly for its type
inference mechanism, that gives type security without overburdening the user.
Types, and especially abstract types, are the basis for distinguishing the
theorems of a logic from arbitrary formulae, in a secure way. A standard has
now been established for ML [4]. The most recent
version of Cambridge LCF, which is documented in Paulson's book
[5], is based on this
Standard ML.
The original HOL system included an earlier version of ML, as did the enhanced
and rationalized version, called HOL88, which was released (in 1988) after
the original HOL system had been in use for several years.
In the early 1990's HOL90, an implementation of HOL based on
Standard ML rather than Lisp, was developed by
Konrad Slind, initially at the
University of Calgary. A commercial version of HOL using Standard ML was also
developed by ICL Secure Systems. This system, now called ProofPower, is a
`highly assured' system for commercial verification projects in the safety and
security critical areas.
- A. Church,
"A Formulation of the Simple Theory of Types",
Journal of Symbolic Logic Vol. 5 (1940), pp. 56-68.
- F. K.
Hanna and N. Daeche,
"Specification and Verification Using Higher-Order Logic: A Case Study".
In Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh
Workshop on VLSI, edited by G. Milne and P. A. Subrahmanyam,
North-Holland, 1986, pp. 179-213.
- M. Gordon,
R. Milner and
C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation,
Lecture Notes in Computer Science, Vol. 78, Springer-Verlag, 1979.
- R. Milner,
M. Tofte and R. Harper, The Definition of Standard ML,
The MIT Press, 1990.
- L. Paulson,
Logic and Computation: Interactive Proof with Cambridge LCF,
Cambridge Tracts in Theoretical Computer Science 2,
Cambridge University Press, 1987.
Systems Related to HOL
There are a number of theorem proving systems related to
the HOL System; some of them are listed below.
Carolyn Talcott and
Michael
Kohlhase have put together a
page on mechanized reasoning.
- ACL2
- ACL2 is a theorem proving system produced at Computational Logic, Inc.
The acronym ``ACL2'' stands for ``A Computational Logic for Applicative Common
Lisp.'' ACL2 is similar to the Boyer-Moore theorem prover,
Nqthm, and
Kaufmann's interactive extension, Pc-Nqthm. However, instead of supporting
the ``Boyer-Moore logic,'' ACL2 supports a large applicative subset of Common
Lisp. Furthermore, ACL2 is programmed almost entirely within that language.
- CLAM
- CLAM is a proof planner from the
Mathematical Reasoning Group
at the Department of Artificial Intelligence, University of Edinburgh.
- Coq
- The Coq proof assistant allows mechanical manipulation of assertions of
the "Calculus of Inductive Constructions", interactive development of formal
proofs, and synthesis of certified programs from the constructive proofs of
their specifications.
- Eves
- Eves is a verification environment, the main component of which is a
theorem prover called Never.
- Gypsy
- Gypsy is a verification environment with its own language.
-
Hol Light
- HOL Light is a computer program to help users prove
interesting mathematical theorems completely formally in
higher order logic.
There are a number of versions of HOL, going back to Mike Gordon's
work in the early 80s. Compared with other HOL systems, HOL Light
uses a much simpler logical core and has little legacy code,
giving the system a simple and uncluttered feel.
- Isabelle
- Isabelle is a generic theorem prover written in
Standard ML. It is
generic in the sense that users can define their own logic using a metalogic.
Isabelle has a number of things in common with HOL: a programming
meta-language, tactics and tacticals, and a fully-expanded proof is generated
(over time). There are also significant differences, e.g., rules are not
implemented as ML functions but are represented as explicit structures, and
higher-order resolution is used for proof construction.
- LAMBDA
- LAMBDA is a commercial system similar to Isabelle but specialised to a
classical higher-order logic with polymorphism like the one mechanised in the
HOL system. Early versions implemented a constructive logic of partial terms.
The system comes with a graphical interface for hardware design called DIALOG.
- LP
- The Larch Prover is an interactive theorem proving system for multisorted
first-order logic.
- Nqthm
(The Boyer-Moore Theorem Prover)
- Nqthm is a theorem proving system for a computational logic. The
logic is (intentionally) similar to the core of the Lisp programming language.
It is untyped, quantifier free, and first order. Nqthm provides a high degree
of automation in terms of heuristics for simplification, induction, and
related activities. A proof in the system is generated by making definitions
and then calling the heuristics on the conjecture to be proved. The proof
attempt will typically fail, but examination of the prover's log (which is in
English) will reveal either a flaw in the conjecture or a lemma that the
prover needs to be aware of to succeed. The user then asks the system to prove
this lemma (possibly requiring other lemmas to be proved) and repeats the
attempt to prove the original conjecture. This process continues until the
prover succeeds on the conjecture.
- Nuprl
- Nuprl is another system descended from LCF. Its
logic is based on Martin-Löf's intuitionistic (constructive) type theory.
The infrastructure of Nuprl has much in common with HOL, but differs in that
proofs are represented explicitly as objects. However, these are not full
proofs in terms of primitive inferences; each node of the proof
tree corresponds to the application of a tactic which might be at a high
level. Nevertheless, this helps users to examine the proof, and facilitates
backtracking and alternative proof attempts.
- OBJ
- OBJ is based on order-sorted equational logic and is organised in
parameterised modules.
- ProofPower
- ProofPower is a commercial implementation of HOL by ICL Secure Systems. It
is being used for formal reasoning about Z specifications.
- PVS
- The Prototype Verification System from SRI International is an interactive
system for a higher order logic with dependent types. It has its own
specification language. Significant automation is achieved using decision
procedures for various theories including linear arithmetic.
- RRL
- Rewrite Rule Laboratory is a theorem prover for first-order logic with an
emphasis on equational reasoning.
- SDVS
- The State Delta Verification System is a verification system that
incorporates simplifiers, decision procedures and symbolic execution. It is
based on a temporal logic and has been mainly used for verification of
computer descriptions written in languages such as Ada and VHDL.
- Veritas
- Veritas is a logic developed by
Keith Hanna to support formal design methods. It is motivated by
Martin-Löf's intuitionistic (constructive) type theory: it is higher
order and provides dependent types and subtypes, but it is a classical rather
than a constructive logic. The Veritas-90 version is implemented in both
Standard ML and
Haskell.
The intention behind the implementation in the purely-functional language
Haskell is to enable parallel evaluation. As in HOL, abstract data types are
used to securely implement the various syntactic categories of the logic, but
in addition to terms and theorems being implemented in this way, so is the
representation of theories, which are first-class objects in Veritas. In HOL,
theories are structures that are modified imperatively. In Veritas, a
purely-functional view is taken.
|