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/axiom-website/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/axiom-website/patches.html 20150505.02.tpd.patch +20150515 tpd books/bookvol13 add Kama15 reference 20150505 tpd src/axiom-website/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/axiom-website/patches.html 20150501.01.tpd.patch 20150501 tpd books/bookvol5 remove saturn 20150501 tpd src/interp/br-con.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 - man-machine 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/axiom-website/patches.html b/src/axiom-website/patches.html index 8cb8cb6..58e6da4 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -5051,7 +5051,9 @@ src/interp/vmlisp.lisp replace stringimage with princ-to-string
20150501.01.tpd.patch src/interp/br-con.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