From 6c620858d2ae5471cf78a7c4ccf830f35178790f Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 5 May 2015 11:56:49 0400
Subject: [PATCH] books/bookvol13 add Kama15 reference
Add Kama15 to the Axiom Proof book.

books/bookvol13.pamphlet  24 ++++++++++++++++++++++++
changelog  4 +++
patch  39 ++
src/axiomwebsite/patches.html  4 +++
4 files changed, 32 insertions(+), 39 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 9d3d770..4a6c499 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 17,6 +17,18 @@ in general but will certainly exist for known algorithms.
Bressoud said:
\begin{quote}
+{\bf Writing is nature's way of letting you know how sloppy your
+thinking is
+}  Guindon\cite{Lamp02}
+\end{quote}
+
+\begin{quote}
+{\bf Mathematics is nature's way of letting you know how sloppy
+your writing is.
+}  Leslie Lamport\cite{Lamp02}
+\end{quote}
+
+\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
@@ 244,6 +256,18 @@ things that are not true. The method, based on hierarchical
structuring, is simple and practical. The author's twenty years of
experience writing such proofs is discussed.
+Lamport points out that proofs need rigor and precision.
+Structure and Naming are important. Every step of the proof
+names the facts it uses.
+
+Temporal Logic of Actions (TLA)
+\begin{quote}
+{\bf Sloppiness is easier than precision and rigor}
+ Leslie Lamport\cite{Lamp14a}
+\end{quote}
+
+Computerising Mathematical Text\cite{Kama15} explores various ways of
+capturing mathematical reasoning.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Bibliography}
diff git a/changelog b/changelog
index aa7cd60..2db984b 100644
 a/changelog
+++ b/changelog
@@ 1,5 +1,7 @@
+20150505 tpd src/axiomwebsite/patches.html 20150505.02.tpd.patch
+20150515 tpd books/bookvol13 add Kama15 reference
20150505 tpd src/axiomwebsite/patches.html 20150505.01.tpd.patch
20150505 tpd books/bookvolbib add Kama14 to paper collection
+20150505 tpd books/bookvolbib add Kama15 to paper collection
20150501 tpd src/axiomwebsite/patches.html 20150501.01.tpd.patch
20150501 tpd books/bookvol5 remove saturn
20150501 tpd src/interp/brcon.lisp remove saturn
diff git a/patch b/patch
index 2f455f1..29311b4 100644
 a/patch
+++ b/patch
@@ 1,38 +1,3 @@
books/bookvolbib add Kama14 to paper collection

@misc{Kama15,
 author = "Kamareddine, Fairouz and Wells, Joe and Zengler, Christoph and
 Barendregt, Henk",
 title = "Computerising Mathematical Text",
 url =
"http://repository.ubn.ru.nl/bitstream/handle/2066/134655/134655.pdf?sequence=1",
 paper = "Kama15.pdf",
 abstract =
 "Mathematical texts can be computerised in many ways that capture
 differing amounts of the mathematical meaning. At one end, there is
 document imag ing, which captures the arrangement of black marks on
 paper, while at the other end there are proof assistants (e.g., Mizar,
 Isabelle, Coq, etc.), which capture the full mathematical meaning and
 have proofs expressed in a formal foundation of mathematics. In
 between, there are computer typesetting systems (e.g., LATEX and
 Presentation MathML) and semantically oriented systems (e.g., Content
 MathML, OpenMath, OMDoc, etc.). In this paper we advocate a style of
 computerisation of mathematical texts which is flexible enough to
 connect the different approaches to computerisation, which allows
 various degrees of formalisation, and which is compatible with
 different logical frameworks (e.g., set theory, category theory, type
 theory, etc.) and proof systems. The basic idea is to allow a
 manmachine collaboration which weaves human input with machine
 computation at every step in the way. We propose that the huge step
 from informal mathematics to fully formalised mathematics be divided
 into smaller steps, each of which is a fully developed method in which
 human input is minimal. Let us consider the following two questions:
 \begin{enumerate}
 \item What is the relationship between the logical foundations of
 mathematical reasoning and the actual practice of mathematicians?
 \item In what ways can computers support the development and
 communication of mathematical knowledge?
 \end{enumerate}"
}

+books/bookvol13 add Kama15 reference
+Add Kama15 to the Axiom Proof book.
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 8cb8cb6..58e6da4 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5051,7 +5051,9 @@ src/interp/vmlisp.lisp replace stringimage with princtostring
20150501.01.tpd.patch
src/interp/brcon.lisp remove saturn
20150505.01.tpd.patch
books/bookvolbib add Kama14 to paper collection
+books/bookvolbib add Kama15 to paper collection
+20150505.02.tpd.patch
+books/bookvol13 add Kama15 reference

1.7.5.4