ACL2 Seminar, 3/29/2019

Speaker: Mertcan Temel

Title: RP-Rewriter: A Knowledge Preserving Rewriter to Reduce Backchaining

Abstract:

Being developed as a proven ACL2 clause processor, this rewriter takes
a term that represents a theorem to be proven, and applies the
existing rewrite rules in the ACL2 world. It works with some of the
heuristics of ACL2's own rewriter but with a more restricted
domain. Differently than ACL2's own rewriter, this rewriter supports
two additional features: 1. It remembers properties for terms in order
to reduce backchaining that may cause a blow up, and 2. It has a
support for fast-alists to help with the performance when rewriting
terms that contain big association lists.  We will use verification of
fast integer multipliers as an example to show the performance
benefits of this rewriter. Additionally, we will talk about the proof
structure and some challenges.