Arithmetic
Libraries for reasoning about basic arithmetic, bit-vector
arithmetic, modular arithmetic, etc.
Subtopics
- 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.
