Sciweavers

ACL2
2006
ACM

Double rewriting for equivalential reasoning in ACL2

14 years 4 months ago
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
Matt Kaufmann, J. Strother Moore
Added 13 Jun 2010
Updated 13 Jun 2010
Type Conference
Year 2006
Where ACL2
Authors Matt Kaufmann, J. Strother Moore
Comments (0)