Edinburgh Research Explorer

System Description: an Interface Between CLAM and HOL

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

Related Edinburgh Organisations

Documents

http://www.springerlink.com/content/buu51mnptynaquuy/
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
Pages134-138
ISBN (Electronic)978-3-540-69110-5
ISBN (Print)978-3-540-64675-4
DOIs
StatePublished - 1998

Publication series

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

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.

Download statistics

No data available

ID: 6328485