DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)

by Matt Kaufmann
Published 2018-10-01

Meta-extract: Using Existing Facts in Meta-reasoning

by Matt Kaufmann, Sol Swords
Published 2017-05-01

Industrial-Strength Documentation for ACL2

by Jared Davis, Matt Kaufmann
Published 2014-06-01

How Can I Do That with ACL2? Recent Enhancements to ACL2

by Matt Kaufmann, J Strother Moore
Published 2011-10-01

Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1

by Matt Kaufmann, J Strother Moore
Published 2013-04-01

Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4

by Matt Kaufmann, J Strother Moore
Published 2014-06-01

A Versatile, Sound Tool for Simplifying Definitions

by Alessandro Coglio, Matt Kaufmann, Eric W. Smith
Published 2017-05-01

Abstract Stobjs and Their Application to ISA Modeling

by Shilpi Goel, Warren A Hunt, Jr., Matt Kaufmann
Published 2013-04-01

Fourier Series Formalization in ACL2(r)

by Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.
Published 2015-09-01

Integrating Testing and Interactive Theorem Proving

by Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios
Published 2011-10-01