From c953f568e22244cd5ebdbecce82718e402417777 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 5 May 2015 11:50:52 -0400
Subject: [PATCH] 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/bookvolbib.pamphlet | 42 ++++++++++++++++++++++++++++++++++++++++
changelog | 2 +
patch | 38 ++++++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
4 files changed, 82 insertions(+), 2 deletions(-)
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index dc2dc3d..1139664 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2801,6 +2801,48 @@ 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,
diff --git a/changelog b/changelog
index 51f2db9..aa7cd60 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20150505 tpd src/axiom-website/patches.html 20150505.01.tpd.patch
+20150505 tpd books/bookvolbib add Kama14 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 1a7ac84..2f455f1 100644
--- a/patch
+++ b/patch
@@ -1,4 +1,38 @@
-src/interp/br-con.lisp remove saturn
+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}"
+}
-The last bits of the saturn interface were removed.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 1dab855..8cb8cb6 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5050,6 +5050,8 @@ src/interp/vmlisp.lisp change prin0 to prin1 everywhere

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

--
1.7.5.4