98 citations · 200 across the 15 of their papers we have counts for
Showing 2017Show all
3 papers · 1 filter
cs.PL2017★ 8 cited
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…
cs.LO2017★ 4 cited
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…
math.LO2017
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…