106 citations · 294 across the 14 of their papers we have counts for
Showing 2017Show all
2 papers · 1 filter
cs.LO2017★ 4 cited
Term-Level Reasoning in Support of Bit-blasting
Sol Swords
GL is a verified tool for proving ACL2 theorems using Boolean methods such as BDD reasoning and satisfiability checking. In its typical operation, GL recursively traverses a term,…
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…