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