an embedding of the acl2 logic in hol
We describe an embedding of the ACL2 logic into higher-order logic. An implementation of this embedding allows ACL2 to be used as an oracle for higher-order logic provers.
acl2 logic hol higher-order logic formal methods first-order logic sound translation proof oracle hol4 verification