Bishop Brock, Matt Kaufmann & J Strother Moore (2008):
Rewriting with Equivalence Relations in ACL2.
Journal of Automated Reasoning 40(4),
pp. 293–306,
doi:10.1007/s10817-007-9095-9.
The ACL2 community:
ACL2 Community Books.
See URL https://code.google.com/p/acl2-books/.
Matt Kaufmann & J Strother Moore:
ACL2 User's Manual.
See URL http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html.
Matt Kaufmann & J Strother Moore:
Rough Diamond: An Extension of Equivalence-based Rewriting.
To appear, Proceedings of ITP 2014.
Matt Kaufmann & J Strother Moore (2011):
How Can I Do That with ACL2? Recent Enhancements to ACL2.
In: David Hardin & Julien Schmaltz: ACL2,
EPTCS 70,
pp. 46–60.
Available at http://dx.doi.org/10.4204/EPTCS.70.4.
Matt Kaufmann & J Strother Moore (2013):
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1.
In: Ruben Gamboa & Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, Laramie, Wyoming, USA , May 30-31, 2013,
Electronic Proceedings in Theoretical Computer Science 114.
Open Publishing Association,
pp. 5–12,
doi:10.4204/EPTCS.114.1.
eptcs@eptcs.org