Linking HOL with Clam
This page is mirrored at:
The official title of this project is Automatic Guidance of Mechanically
Generated Proofs and it was funded by the
Engineering and Physical Sciences Research
Council of Great Britain under grants GR/L03071 (Cambridge) and GR/L14381
The project began in October 1996 and ran for 3 years.
A (socket-based) link between the two systems was designed and built. HOL
goals are translated into the problem format of Clam, and, if Clam succeeds,
the resulting proof plan is translated into a HOL tactic that is expected to
solve the goal. Clam and HOL can also engage in a dialogue that allows HOL to
perform parts of the proof that Clam believes it is better at, and to provide
additional information to Clam in a dynamic way.
Some of the results of the project have fed into ESPRIT Framework IV Project
LTR 26241 "PROSPER".
The way the system operates can perhaps be understood by examining the
is a general-purpose proof system for classical, higher-order predicate
calculus. The HOL system has often been criticized on the basis
that it does not provide a high level of proof automation. Such remarks
are often based on ignorance, since the HOL system provides powerful
simplifiers, automatic first order provers (both tableaux and model
elimination), a semi-decision procedure for a useful fragment of
arithmetic, and a cooperating decision procedure mechanism. However, HOL
lacks automation for many important areas, including induction.
Clam is a
system for Oyster, a tactic-based
implementation of the constructive type theory of Martin-Löf. Clam works
by using formalized pre- and post-conditions of Oyster tactics as the basis of
plan search. When a plan for a goal is found, the expectation is that
the resulting tactic will solve the goal. Experience shows that the search
space for plans is often small enough to allow a plan to be found
automatically in a practical amount of time. One emphasis on research with
Clam has been the automation of inductive proofs using
We have written a short description of the system:
and a more detailed paper:
- System Description: An Interface between CLAM and HOL
- Konrad Slind, Mike Gordon, Richard Boulton, and
In C. Kirchner and H. Kirchner (editors),
Proceedings of the Fifteenth
International Conference on Automated Deduction (CADE-15),
Lindau, Germany, July 1998.
Lecture Notes in Artificial Intelligence
pages 134-138, Springer.
Extended interaction is described in the following paper:
- An Interface between CLAM and HOL
- Richard Boulton, Konrad Slind, Alan Bundy, and
In J. Grundy and
M. Newey (editors),
Proceedings of the 11th
International Conference on Theorem Proving in Higher Order Logics
Canberra, Australia, September/October 1998.
Lecture Notes in Computer Science volume 1479, pages 87-104, Springer.
- Iterative Dialogues and Automated Proof
- Konrad Slind and Richard Boulton
In Proceedings of the Second
International Workshop on Frontiers of Combining Systems (FroCoS'98),
Amsterdam, The Netherlands, October 1998.
Getting the System
Click on a version number in the table below to access the ftp directory for
that version of the HOL/Clam system and read the README file.
||11 Aug 2000
The protagonists in the project were:
Some Related Work
Last modified by Richard Boulton on 3 January 2001