The Milawa Rewriter and an ACL2 Proof of its Soundness
Jared Davis · 2013
Abstract. Rewriting with lemmas is a central strategy in interactive theorem provers. We describe the Milawa rewriter, which makes use of assumptions, cal-culation, and conditional rewrite rules to simplify the terms of a first-order logic. We explain how we have developed an ACL2 proof showing the rewriter is sound, and how this proof can accommodate our rewriter’s many useful features such as free-variable matching, ancestors checking, syntatic restrictions, caching, and forcing.