Libraries for reasoning about basic arithmetic, bit-vector arithmetic, modular arithmetic, etc.

- Lispfloat
- A library for computing with (but not reasoning about) Common Lisp floats from within ACL2.
- Arithmetic-1
- 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. - Number-theory
- Some utilities related to number theory
- Proof-by-arith
- Attempt to prove a theorem using various arithmetic libraries
- Arith-equivs
- Definitions for congruence reasoning about integers/naturals/bits.
- Include-an-arithmetic-book
- Macros for including arithmetic books
- Number-theory
- Quadratic Reciprocity Theorem and other facts from Number Theory
- Arithmetic-3
- Another newer arithmetic library that is considered deprecated in favor of arithmetic-5.
- Arithmetic-2
- A newer arithmetic library that is considered deprecated in favor of arithmetic-5.
- Arithmetic-light
- An arithmetic library developed using a lightweight approach
- Arithmetic-5
- A powerful arithmetic library.