The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #854

Title:A Prototype Interface Between Clam and Hol
Authors:Boulton,R; Bundy,A; Slind,K; Gordon,M
Date:Jun 1997
Presented:To be presented at the 1997 International Conference on Theorem Proving in Higher Order Logics
Abstract:This paper describes a prototype interface between the CLAM proof planner and the HOL interactive theorem prover. CLAM uses artificial intelligence planning techniques to find proofs at a high-level, expecially where inductive proofs are required. HOL is a theorem prover for a classical higher-order logic and has been widely used in both academia and industry for verification of hardware and software. The interface sends HOL goals to CLAM for planning, and translates plans back into HOL tactics that solve the initial goals.

[Search These Pages] [DAI Home Page] [Comment]