		Search-engine friendly clone of the ACL2 documentation.

Pub-papers

Pub-capabilities

ACL2 Capabilities

Rough Diamond: An Extension of Equivalence-based Rewriting, Matt Kaufmann and J Strother Moore. Proceedings of ITP 2014, 5th Conference on Interactive Theorem Proving, Gerwin Klein and Ruben Gamboa, editors. LNCS 8558 pp. 537-542, Springer International Publishing, 2014. Also see http://dx.doi.org/10.1007/978-3-319-08970-6_35.
A Futures Library and Parallelism Abstractions for a Functional Subset of Lisp, David L. Rager, Warren A. Hunt, Jr. and Matt Kaufmann. In Proceedings of ELS 2011 (4th European Lisp Symposium), pp. 13--16, March 31 -- April 1, 2011, Hamburg, Germany. This paper is relevant to ACL2(p), the experimental extension of ACL2 supporting parallel evaluation and proof (see parallelism).
Rewriting with Equivalence Relations in ACL2, Bishop Brock, Matt Kaufmann, and J Strother Moore. Journal of Automated Reasoning 40 (2008), pp. 293-306.
Proof Search Debugging Tools in ACL2, Matt Kaufmann and J Strother Moore. Unpublished, but presented in a talk at Tools and Techniques for Verification of System Infrastructure, A Festschrift in honour of Prof. Michael J. C. Gordon FRS (Richard Boulton, Joe Hurd, and Konrad Slind, organizers). March 25-26, 2008, Royal Society, London.
Efficient execution in an automated reasoning environment, David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, Jose' Luis Ruiz-Reina, Rob Sumners, Daron Vroon and Matthew Wilding. Journal of Functional Programming, Volume 18, Issue 01, January 2008. Cambridge University Press.
Double Rewriting for Equivalential Reasoning in ACL2, Matt Kaufmann and J Strother Moore. In P. Manolios and M. Wilding (eds.), Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, pages 103-106. Proceeding have also been published in the ACM Digital Library. Copyright ACL2 Steering Committee.
Linear and Nonlinear Arithmetic in ACL2, Warren A. Hunt Jr., Robert Bellarmine Krug, and J Moore. In CHARME 2003, D. Geist (ed.), Springer Verlag LNCS 2860, pp. 319-333, 2003. This paper describes the mechanization of linear and nonlinear arithmetic in ACL2.
Integrating Nonlinear Arithmetic into ACL2, Warren A. Hunt Jr., Robert Bellarmine Krug, and J Moore. In Proceedings of ACL2 Workshop 2004. This paper presents an overview of the integration of a nonlinear arithmetic reasoning package into ACL2.
Meta Reasoning in ACL2, Warren A. Hunt Jr, Matt Kaufmann, Robert Bellarmine Krug, J Moore, and Eric W. Smith. In 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer Lecture Notes in Computer Science, 3603, pp. 163--178, 2005. This paper describes the variety of meta-reasoning facilities in ACL2.