System Description: an Interface Between CLAM and HOL

K. Slind; M. Gordon; R. Boulton; Alan Bundy

doi:10.1007/BFb0054255

System Description: an Interface Between CLAM and HOL

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Export citation
[ RIS ]
[ BibTeX ]

K. Slind
M. Gordon
R. Boulton
Alan Bundy

Related Edinburgh Organisations

School of Informatics

Documents

Download as Adobe PDF
Submitted manuscript, 137 KB, PDF document

http://www.springerlink.com/content/buu51mnptynaquuy/

Original language	English
Title of host publication	Automated Deduction — CADE-15
Subtitle of host publication	15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998 Proceedings
Publisher	Springer-Verlag GmbH
Pages	134-138
ISBN (Electronic)	978-3-540-69110-5
ISBN (Print)	978-3-540-64675-4
DOIs	https://doi.org/10.1007/BFb0054255
Publication status	Published - 1998

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	1421
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