System Description: an Interface Between CLAM and HOL

Proceedings of CADE-15

dc.contributor.author	Alan, Bundy	en
dc.contributor.author	Slind, K.	en
dc.contributor.author	Gordon, M.	en
dc.contributor.author	Boulton, R.	en
dc.date.accessioned	2011-01-31T12:55:16Z
dc.date.available	2011-01-31T12:55:16Z
dc.date.issued	1998
dc.identifier.uri	http://www.springerlink.com/content/buu51mnptynaquuy/
dc.identifier.uri	http://hdl.handle.net/1842/4708
dc.description.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.	en
dc.language.iso	en
dc.publisher	Springer Verlag	en
dc.title	System Description: an Interface Between CLAM and HOL	en
dc.type	Article	en
rps.volume	1421	en
rps.title	Proceedings of CADE-15	en
dc.date.updated	2011-01-31T12:55:17Z