From ffcb776d1ddf80cf96810f855d7230ee790eddf1 Mon Sep 17 00:00:00 2001 From: Tim Daly Date: Fri, 8 May 2015 05:13:31 -0400 Subject: [PATCH] books/bookvolbib add Robe15 reference @misc{Robe15, author = "Roberts, Siobhan", title = "In Mathematics, Mistakes Aren't What They Used To Be", year = 2015, url = "http://nautil.us/issue/24/error/In-mathematics-mistakes-arent-what-they-used-to-be" --- books/bookvolbib.pamphlet | 53 ++++++++------------------------------- changelog | 2 + patch | 9 +++++- src/axiom-website/patches.html | 2 + 4 files changed, 22 insertions(+), 44 deletions(-) diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet index 1139664..d687618 100644 --- a/books/bookvolbib.pamphlet +++ b/books/bookvolbib.pamphlet @@ -2801,48 +2801,6 @@ FME'99, Toulouse, France, Sept 20-24, 1999, pp 1758-1777 \end{chunk} -\index{Kamareddine, Fairouz} -\index{Wells, Joe} -\index{Zengler, Christoph} -\index{Barendregt, Henk} -\begin{chunk}{axiom.bib} -@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}" -} - -\end{chunk} - \index{Lamport, Leslie} \begin{chunk}{axiom.bib} @book{Lamp02, @@ -3070,6 +3028,17 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael \end{chunk} +\index{Roberts, Siobhan} +\begin{chunk}{axiom.bib} +@misc{Robe15, + author = "Roberts, Siobhan", + title = "In Mathematics, Mistakes Aren't What They Used To Be", + year = 2015, + url = "http://nautil.us/issue/24/error/In-mathematics-mistakes-arent-what-they-used-to-be" +} + +\end{chunk} + \section{Interval Arithmetic} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \index{Boehm, Hans-J.} diff --git a/changelog b/changelog index 2db984b..c225ca1 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,5 @@ +20150508 tpd src/axiom-website/patches.html 20150508.01.tpd.patch +20150508 tpd books/bookvolbib add Robe15 reference 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 diff --git a/patch b/patch index 29311b4..d09c818 100644 --- a/patch +++ b/patch @@ -1,3 +1,8 @@ -books/bookvol13 add Kama15 reference +books/bookvolbib add Robe15 reference + +@misc{Robe15, + author = "Roberts, Siobhan", + title = "In Mathematics, Mistakes Aren't What They Used To Be", + year = 2015, + url = "http://nautil.us/issue/24/error/In-mathematics-mistakes-arent-what-they-used-to-be" -Add Kama15 to the Axiom Proof book. diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index 58e6da4..129f8e1 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -5054,6 +5054,8 @@ src/interp/br-con.lisp remove saturn
books/bookvolbib add Kama15 to paper collection
20150505.02.tpd.patch books/bookvol13 add Kama15 reference
+20150508.01.tpd.patch +books/bookvolbib add Robe15 reference
-- 1.7.5.4