Edinburgh Research Explorer

System Description: an Interface Between CLAM and HOL

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations


Original languageEnglish
Title of host publicationAutomated Deduction — CADE-15
Subtitle of host publication15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings
PublisherSpringer-Verlag GmbH
ISBN (Electronic)978-3-540-69110-5
ISBN (Print)978-3-540-64675-4
Publication statusPublished - 1998

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
ISSN (Print)0302-9743


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.

Download statistics

No data available

ID: 6328485