How can I do that with ACL2? Recent enhancements to ACL2

DOI10.4204/eptcs.70.4MaRDI QIDQ6586531zbMATH OpenFDO

Authors Matt Kaufmann, J Strother Moore

Publication date 13 August 2024

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Enhancements to ACL2 in versions 5.0, 6.0, and 6.1
• Milestones from the Pure Lisp Theorem Prover to ACL2
• ACL2(ml): machine-learning for ACL2
• An ACL2 Tutorial
• Meta-extract: using existing facts in meta-reasoning

Cites work

• scientific article; zbMATH DE number 46981 (Why is no real title available?)
• Integrating testing and interactive theorem proving

Cited in

(5)

• ACL2(ml): machine-learning for ACL2
• Meta-extract: using existing facts in meta-reasoning
• A macro for reusing abstract functions and theorems
• Enhancements to ACL2 in versions 5.0, 6.0, and 6.1
• Verified AIG algorithms in ACL2

This page was built for publication: How can I do that with ACL2? Recent enhancements to ACL2

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6586531)