Name
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 the initial goals. The project homepage can be found
at http://www.cl.cam.ac.uk/Research/HVG/Clam.HOL/intro.html.
|
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/BFb0054255 | CADE |
Keywords | Field | DocType |
system description,theorem prover,formal verification | HOL,Intuitionistic type theory,Computer science,Concrete syntax,Automated theorem proving,Planner,Algorithm,Proof planning,Formal verification,Proof assistant | Conference |
ISBN | Citations | PageRank |
3-540-64675-2 | 8 | 0.58 |
References | Authors | |
4 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Konrad Slind | 1 | 577 | 55.90 |
| Michael J. C. Gordon | 2 | 463 | 54.17 |
| Richard J. Boulton | 3 | 255 | 23.64 |
| A. Bundy | 4 | 3713 | 532.03 |