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/axiom-website/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 all-purpose 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/axiom-website/patches.html 20150122.01.tpd.patch +20150122 tpd books/bookvol13 update the proof volume 20150121 tpd src/axiom-website/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/axiom-website/patches.html b/src/axiom-website/patches.html index 30807d0..b9732dd 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/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