98 citations · 200 across the 15 of their papers we have counts for
16 papers
Iteration in ACL2
Matt Kaufmann, J Strother Moore
Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- pro…
Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications
Shilpi Goel, Matt Kaufmann
This volume contains the proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2018), a two-day workshop held in Austin, Texas,…
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)
Matt Kaufmann
We present a tool that automates termination proofs for recursive definitions by mining existing termination theorems.
A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann, Eric W. Smith
We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old…
Meta-extract: Using Existing Facts in Meta-reasoning
Matt Kaufmann, Sol Swords
ACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class :meta or :clause-processor ar…
Iterated Ultrapowers for the Masses
Ali Enayat, Matt Kaufmann, Zachiri McKenzie
We present a novel, perspicuous framework for building iterated ultrapowers. Furthermore, our framework naturally lends itself to the construction of a certain type of order indisc…