Parameterized congruences in ACL2

12 years 5 months ago
Parameterized congruences in ACL2
Support for congruence-based rewriting is built into ACL2. This capability allows ACL2 to treat certain predicate relations ”just like equality” under appropriate conditions and allows specific theorems involving those equivalence relations to be used as rewrite rules to guide the simplification process. Although this has proven to be an extremely powerful capability, it comes with limitations. One significant limitation is that equivalence relations cannot be parameterized. This precludes one very natural application of congruences: their use in reasoning about arbitrary modulus arithmetic. We have developed a technique for emulating parameterized congruence-based rewriting on a stock ACL2 system using binding hypotheses and bind-free. We have also developed a library (nary) that provides a means of expressing and utilizing such congruences with a high degree of automation. We demonstrate the application of this library to problems in modular arithmetic and other similar domai...
David Greve
Added 13 Jun 2010
Updated 13 Jun 2010
Type Conference
Year 2006
Where ACL2
Authors David Greve
Comments (0)