Technical reports

Linking ACL2 and HOL

Mark Staples

November 1999, 23 pages

DOI: 10.48456/tr-476

Abstract

This report describes ACL2PII, a system which dynamically links the theorem provers ACL2 and Hol, using the PROSPER project’s Plug-In interface to Hol. The focus of the system is on making ACL2 theorems available from within Hol. In a motivating example we show how to transfer results from ACL2’s ‘small machine’ theory. This theory highlights two of ACL2’s strengths: symbolic simulation and the fast execution of operationally defined functions. This allows ACL2 specifications to be readily validated against real world requirements. The ACL2PII system allows Hol users to capitalise on results about such ACL2 specifications. ACL2 and Hol are both general purpose theorem provers, but Hol is slightly more expressive, and has growing infrastructure for interoperability with other systems. This report assumes a passing knowledge of both ACL2 and Hol.

Full text

PDF (1.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-476,
  author =	 {Staples, Mark},
  title = 	 {{Linking ACL2 and HOL}},
  year = 	 1999,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-476.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-476},
  number = 	 {UCAM-CL-TR-476}
}