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 |
| Keywords: | |
| 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. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}