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...

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: David Greve
• Keywords: ACL2 2006, Certain Predicate Relations, Computational Linguistics, Congruence-based Rewriting, Equivalence Relations