Double rewriting for equivalential reasoning in ACL2

Several users have had problems using equivalence-based rewriting in ACL2 because the ACL2 rewriter caches its results. We describe this problem in some detail, together with a partial solution first implemented in ACL2 Version 2.9.4. This partial solution consists of a new primitive, double-rewrite, together with a new warning to suggest possible use of this primitive. Categories and Subject Descriptors F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—computational logic, mechanical theorem proving General Terms Verification Keywords Verification, formal methods, rewriting, congruences, equivalence relations, double-rewrite

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Matt Kaufmann, J. Strother Moore
• Keywords: ACL2, ACL2 2006, Computational Linguistics, Equivalence-based Rewriting, Partial Solution