Matt Kaufmann, J Strother Moore
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.
Matt Kaufmann, J Strother Moore
We report on improvements to ACL2 made since the 2013 ACL2 Workshop.
J Strother Moore, Claus-Peter Wirth
We review the history of the automation of mathematical induction
Matt Kaufmann, J Strother Moore
We 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.