Libraries for reasoning about basic arithmetic, bit-vector
arithmetic, modular arithmetic, etc.
- A library for computing with (but not reasoning about) Common Lisp
floats from within ACL2.
- The classic books/arithmetic library is fast and lightweight.
It provides only modest support for reasoning about how basic operations like
<, +, -, *, /, and expt relate to one
another over integers, rationals, and (for ACL2(r) users) the reals.
- Some utilities related to number theory
- Attempt to prove a theorem using various arithmetic libraries
- Definitions for congruence reasoning about integers/naturals/bits.
- Macros for including arithmetic books
- Quadratic Reciprocity Theorem and other facts from Number Theory
- Another newer arithmetic library that is considered deprecated in favor of arithmetic-5.
- A newer arithmetic library that is considered deprecated in favor of arithmetic-5.
- An arithmetic library developed using a lightweight approach
- A powerful arithmetic library.