Linking HOL with Clam

This page is mirrored at:
Cambridge: http://www.cl.cam.ac.uk/Research/HVG/Clam.HOL/
Edinburgh: http://dream.dai.ed.ac.uk/software/systems/hol-clam/

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 (Edinburgh).

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".

System Operation

The way the system operates can perhaps be understood by examining the following diagram:

system picture

Background

HOL 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 proof planning 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 rippling.

Papers

We have written a short description of the system:
System Description: An Interface between CLAM and HOL
Konrad Slind, Mike Gordon, Richard Boulton, and Alan Bundy
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 volume 1421, pages 134-138, Springer.
and a more detailed paper:
An Interface between CLAM and HOL
Richard Boulton, Konrad Slind, Alan Bundy, and Mike Gordon
In J. Grundy and M. Newey (editors), Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98), Canberra, Australia, September/October 1998.
Lecture Notes in Computer Science volume 1479, pages 87-104, Springer.
Extended interaction is described in the following paper:
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.
Gzipped PostScript

Project Documentation

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.

Version Release Date Planner Proof Checker
1.02 11 Aug 2000 Clam HOL90.10

People

The protagonists in the project were:
Richard Boulton, boulton@dcs.gla.ac.uk
Alan Bundy, bundy@dai.ed.ac.uk
Mike Gordon, Mike.Gordon@cl.cam.ac.uk
Konrad Slind, Konrad.Slind@cl.cam.ac.uk

Some Related Work
Last modified by Richard Boulton on 3 January 2001