From 5a61d5fd1cb1a832e355905145e751a6e15c39b7 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Thu, 22 Jan 2015 00:11:18 0500
Subject: books/bookvol13 update the proof volume

books/bookvol13.pamphlet  26 ++++++++++++++++++++++++++
changelog  2 ++
patch  6 +
src/axiomwebsite/patches.html  2 ++
4 files changed, 31 insertions(+), 5 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index bd5ef43..95a403a 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 4,6 +4,32 @@
\input{bookheader.tex}
\mainmatter
\setcounter{chapter}{0} % Chapter 1
+Ultimately we would like Axiom to be able to prove that an
+algorithm generates correct results. There are many steps
+between here and that goal, including proving one Axiom
+algorithm correct through all of the levels from Spad code,
+to the Lisp code, to the C code, to the machine code; a
+daunting task of its own.
+
+The proof of a single Axiom algorithm is done with an eye toward
+automating the process. Automated machine proofs are not possible
+in general but will certainly exist for known algorithms.
+Bressoud said:
+
+\begin{quote}
+{\bf
+The existence of the computer is giving impetus to the discovery of
+algorithms that generate proofs. I can still hear the echos of the
+collective sigh of relief that greeted the announcement in 1970 that
+there is no general algorithm to test for integer solutions to
+polynomial Diophantine equations; Hilbert's tenth problem has no
+solution. Yet, as I look at my own field, I see that creating
+algorithms that generate proofs constitutes some of the most important
+mathematics being done. The allpurpose proof machine may be dead, but
+tightly targeted machines are thriving.}
+ Dave Bressoud \cite{Bres93}
+\end{quote}
+
\begin{quote}
{\bf In contrast to humans, computers are good at performing formal
processes. There are people working hard on the project of actually
diff git a/changelog b/changelog
index 6d7a616..a97a6cf 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20150122 tpd src/axiomwebsite/patches.html 20150122.01.tpd.patch
+20150122 tpd books/bookvol13 update the proof volume
20150121 tpd src/axiomwebsite/patches.html 20150121.02.tpd.patch
20150121 tpd books/bookvol10.3 add Hex String to Integer conversion
20150121 tpd src/input/Makefile copy .eps files to doc
diff git a/patch b/patch
index cd9b6bd..9e364c1 100644
 a/patch
+++ b/patch
@@ 1,6 +1,2 @@
books/bookvol10.3 add Hex String to Integer conversion

The toint: String > Integer changes a String of Hex Characters
into an Integer; useful for cryptographic work.

+books/bookvol13 update the proof volume
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 30807d0..b9732dd 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 4966,6 +4966,8 @@ src/input/bitcoin.input demonstrate finite fields and graphics
src/input/bitcoin.input add additional information
20150121.02.tpd.patch
books/bookvol10.3 add Hex String to Integer conversion
+20150122.01.tpd.patch
+books/bookvol13 update the proof volume

1.7.5.4