Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore & Eric Whitman Smith (2005):
Meta Reasoning in ACL2.
In: Joe Hurd & Tom Melham: Theorem Proving in Higher Order Logics.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 163–178,
doi:10.1007/11541868_11.
Matt Kaufmann & J. Strother Moore (2014):
Rough Diamond: An Extension of Equivalence-Based Rewriting.
In: Gerwin Klein & Ruben Gamboa: Interactive Theorem Proving.
Springer International Publishing,
Cham,
pp. 537–542,
doi:10.1007/978-3-319-08970-6_35.
Matt Kaufmann, J Strother Moore, Sandip Ray & Erik Reeber (2009):
Integrating external deduction tools with ACL2.
Journal of Applied Logic 7(1),
pp. 3 – 25,
doi:10.1016/j.jal.2007.07.002.
Special Issue: Empirically Successful Computerized Reasoning.
David M. Russinoff (2019):
Formal Verification of Floating-Point Hardware Design: A Mathematical Approach.
Springer,
doi:10.1007/978-3-319-95513-1.
Sol Swords (2017):
Term-Level Reasoning in Support of Bit-blasting.
In: Anna Slobodova & Warren A. Hunt, Jr.: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017,
Electronic Proceedings in Theoretical Computer Science 249.
Open Publishing Association,
pp. 95–111,
doi:10.4204/EPTCS.249.7.
Sol Swords & Jared Davis (2011):
Bit-Blasting ACL2 Theorems.
In: David Hardin & Julien Schmaltz: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, November 3-4, 2011,
Electronic Proceedings in Theoretical Computer Science 70.
Open Publishing Association,
pp. 84–102,
doi:10.4204/EPTCS.70.7.