Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #885 | |
|---|---|
| Title: | System Description: an Interface Between Clam and Hol |
| Authors: | Slind,K; Gordon,M; Boulton,R; Bundy,A |
| Date: | Jan 1998 |
| Presented: | Submitted to CADE-15 |
| Keywords: | |
| Abstract: | The CLAM proof planner has been interfaced to the HOL interactive theorem prover to provide the power of proof planning to people using HOL for formal verification, etc. the interface sends HOL goals to CLAM for planning and translates plans back into HOL tactics that solve initial goals. The project homepage can be found at http://www.cl.cam.ac.uk/Research/HVG/Clam.HOL/intro.html. |
| 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}