4 citations · 4 across the 1 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2020★ 4 cited
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…
cs.LO2018
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.
cs.LO2017
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…