An embedding of the ACL2 logic in HOL

We describe an embedding of the ACL2 logic into higherorder logic. An implementation of this embedding allows ACL2 to be used as an oracle for higher-order logic provers. Categories and Subject Descriptors F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—computational logic, mechanical theorem proving; D.3.1 [Programming Languages]: Formal Definitions and Theory—semantics General Terms Languages, Security, Theory, Verification Keywords Verification, formal methods, logic, ACL2, HOL, HOL4, first-order logic, higher-order logic, sound translation, proof oracle

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds
• Keywords: ACL2 2006, ACL2 Logic, Computational Linguistics, Mathematical Logic—computational Logic, first-order Logic