System Description: an Interface Between CLAM and HOL

Edinburgh Research Archive

Please use this identifier to cite or link to this item: http://hdl.handle.net/1842/4708

This item has been viewed 6 times in the last year. View Statistics

Files in This Item:

File	Description	Size	Format
BundyA_System Description.pdf		87.12 kB	Adobe PDF	View/Open

Title:	System Description: an Interface Between CLAM and HOL
Authors:	Alan, Bundy Slind, K. Gordon, M. Boulton, R.
Issue Date:	1998
Journal Title:	Proceedings of CADE-15
Volume:	1421
Publisher:	Springer Verlag
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.
URI:	http://www.springerlink.com/content/buu51mnptynaquuy/ http://hdl.handle.net/1842/4708
Appears in Collections:	Informatics Publications