Add to Chrome
Add to Firefox
Add to EdgeJ Strother Moore
Advances in ACL2 Proof Debugging Tools
Nov 15, 2023
The experience of an ACL2 user generally includes many failed proof attempts. A key to successful use of the ACL2 prover is the effective use of tools to debug those failures. We focus on changes made after ACL2 Version 8.5: the improved break-rewrite utility and the new utility, with-brr-data.
* In Proceedings ACL2-2023, arXiv:2311.08373
Automation of Mathematical Induction as part of the History of Logic
Jul 28, 2014
We review the history of the automation of mathematical induction
* ii+107 pages
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
Jun 06, 2014We report on improvements to ACL2 made since the 2013 ACL2 Workshop.
* In Proceedings ACL2 2014, arXiv:1406.1238
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1
Apr 30, 2013We report on highlights of the ACL2 enhancements introduced in ACL2 releases since the 2011 ACL2 Workshop. Although many enhancements are critical for soundness or robustness, we focus in this paper on those improvements that could benefit users who are aware of them, but that might not be discovered in everyday practice.
* In Proceedings ACL2 2013, arXiv:1304.7123