1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
Advice on the use of arithmetic books (based largely on comments from
Robert Krug, and repeated in ../arithmetic-5/README):
SUMMARY: Power users should include arithmetic-5/top; new users
should probably instead include arithmetic/top-with-meta.
Details:
If you are willing to use dmr (see :doc dmr) and tolerate
sometimes-slower (but more complete) reasoning, use arithmetic-5.
Robert is not aware of any rewriting loops.
Don't use arithmetic-3. It's not as powerful as arithmetic-5
(Robert doesn't know if it's faster), and it may have more rewriting
loops than arithmetic-5.
Note that arithmetic-2 is totally obsolete. We may stop
distributing it.
If you want fast, lightweight arithmetic, use
arithmetic/top-with-meta.
============================================================
Please see Section 0 of ../arithmetic-5/README for information about
which arithmetic books to use.
Contents of this directory:
README This file
abs.lisp Theorems about absolute value
binomial.lisp A proof of the binomial theorem
certify.lsp (ld "certify.lsp") to certify books in this directory
equalities.lisp Arithmetic equality rules
factorial.lisp Theorems about the factorial function
idiv.lisp Theorems about integer division and related functions
inequalities.lisp Arithmetic inequality rules
nat-listp.lisp Book about lists of natural numbers
rational-listp.lisp Very short book about lists of rationals
rationals-with-axioms-proved.lisp Supersedes rationals-with-axioms.lisp
sumlist.lisp Theorems about sum of a list of numbers
top.lisp Putting it all together
top-with-meta.lisp Extension of top.lisp by the books in ../meta
Many people contributed to these books, especially
Bishop Brock
John Cowles
Matt Kaufmann
Art Flatau
Ruben Gamboa
|
