Skip to content
Snippets Groups Projects
Commit b516f2ac authored by m-iancu's avatar m-iancu
Browse files

more

parent 36810378
No related branches found
No related tags found
No related merge requests found
......@@ -11,7 +11,7 @@ contribution in the commons. It is the realms structure with its equivalent pill
abstraction capabilities that gives the recaps the necessary flexibility to adequately
model the variety of anchors we see in mathematical documents.
We have validated our model by identifying the recaps and their types in 15 recent papers
We have validated our model by identifying the recaps and their types in 30 recent papers
randomly selected from a preprint archive. To obtain a more scientific evaluation of the
model, we need a much larger and more varied sample. We are currently developing an
annotation ontology for realms and recaps for the KAT annotator~\cite{DumGinKoh:katsd14}
......
......@@ -44,17 +44,17 @@ checker.
On the other hand, libraries of formalized mathematics directly represent the structure
of a mathematical knowledge commons, usually in graph of files and file inclusions or a
graph of theories and theory morphisms (see ~\cite{RabKoh:WSMSML13} for a survey). The
respective graphs supply identifiers for knowledge items detail their relations to each
respective graphs supply identifiers for knowledge items and detail their relations to each
other.
It stands to reason that the two dissemination and aggregation approaches can profit from
each other. The scientific publication process can profit from a more explicitly
represented knowledge commons, which enables added-value services for finding,
understanding, and applying relevant knowledge items -- after all the document/knowledge
space even in mathematics is much to large and complex for a single human to process. Of
space even in mathematics is much too large and complex for a single human to process. Of
course a prerequisite for this is computer support in the aggregation of the knowledge
space. Conversely, formal libraries can profit from a dissemination process based on the
publication self-contained documents to scale the secondary aspects (quality control,
publication of self-contained documents to scale the secondary aspects (quality control,
checkpointing, citation stability, persistence, attention management) of assembling large
bodies of knowledge. Even though formal developments are machine-checkable, their
authoring, maintenance, refactoring, \ldots are processes that need at least some human
......
@Comment{$ biblatex control file $}
@Comment{$ biblatex version 2.3 $}
Do not modify this file!
This is an auxiliary file used by the 'biblatex' package.
This file may safely be deleted. It will be recreated as
required.
@Control{biblatex-control,
options = {2.3:0:0:1:0:0:1:1:0:1:0:0:12:1:3:1:79:+},
}
No preview for this file type
......@@ -9,6 +9,7 @@
\usepackage[show]{ed}
\usepackage{paralist}
\usepackage{listings}
\usepackage{caption,subcaption}
\usepackage[linkcolor=black]{hyperref}
......@@ -71,10 +72,6 @@
\end{abstract}
%\setcounter{tocdepth}{3}\tableofcontents\newpage
\ednote{MK@MI: capitalize all captions}
\ednote{MK@MI: I have xscaled all figures, that should make them more amenable to
side-by-side treatment, but they need to be tweaked a bit still}
\section{Introduction}\label{sec:intro}
\input{intro}
......
This diff is collapsed.
......@@ -33,8 +33,8 @@ Mathematical documents traditionally have:
\begin{inparaenum}[\em i\rm)]
\item recapitulates or surveys concepts and results from the documents/knowledge commons
to make the document self-contained (for its intended audience)
\item identifies any assumptions and give the ensuing contributions a sound
terminological basis
\item identifies any assumptions and gives the ensuing contributions a sound
terminological basis.
\end{inparaenum}
\item\label{md:contri} The \defemph{contributions} part, which contains the development of
new knowledge in form of e.g. new insights, new interpretations of known concepts, new
......@@ -42,7 +42,7 @@ Mathematical documents traditionally have:
\item\label{md:eval} An \defemph{evaluation} of the contributions in terms of
applicability or usability.
\item\label{md:relwork} A discussion of \defemph{related work} which reviews the
contributions and their relation to existing approaches and results from the literature
contributions and their relation to existing approaches and results from the literature.
\item\label{md:concl} A \defemph{conclusion} which summarizes the contribution with the
benefit of hindsight and relates it to the claims made in the introduction.
\item\label{md:aux} Literature references, an index, a glossary, etc. and possibly
......@@ -50,7 +50,7 @@ Mathematical documents traditionally have:
\end{compactenum}
Even though the form or order of the structural elements may vary over publication venues,
and certain elements may be implicit or even missing altogether, the overall structure is
surprisingly stable.
generally stable.
It may be surprising that only one in eleven parts of a mathematical document -- the
``contributions'' -- arguably the largest -- is fully dedicated to transporting the
......@@ -65,7 +65,7 @@ analyze in more detail next.
\subsection{Common Ground/Recapitulation in Mathematical Research}\label{sec:cg-preprints}
To get an overview over recaps in the literature, we randomly selected 15 papers from the
To get an overview over recaps in the literature, we randomly selected 30 papers from the
new submissions to \url{http://arxiv.org/archive/math} and analyzed their structure. All
had a significant common ground section that recapitulates the central notions and fixes
notations. We show two examples where the mathematics involved is relatively elementary.
......@@ -114,7 +114,7 @@ terminology and definitions is not direct, but involves a choice.
define multinets. Here we present them using pencils of plane curves.}''
\end{example}
The next example is not from our 15 examples, since we want to show an even more complex
The next example is not from our 30 examples, since we want to show an even more complex
situation.
\begin{example}\label{ex:atm}
......@@ -211,17 +211,17 @@ the courses become insular; how are students going to communicate with mathemati
have learned their maths from other courses? This is where alluding to the literature
comes in, by connecting the course notes with it.
\begin{newpart}{MK: re-read}
\begin{example}\label{ex:rudin}
The situation in mathematical textbooks is similar in structure to that in research
papers --perhaps more pronounced. Consider the following passage from Rudin's classical
introductory textbook to Functional Analysis~\cite[p. 6f]{Rudin:fa73}.
\begin{labeledquote}\label{q:topspace}\sf
\textbf{1.5 Topological spaces} A \emph{topological space} is a set $S$ in which a
collection $\tau$ of subsets (called \emph{open sets}) has been specified, with the
following properties: $S$ is open, $\emptyset$ is open, [\ldots] Such a collection is
called a \emph{topology} on $S$. [\ldots]
\end{labeledquote}
\ednote{@MK: this looks like something is missing}
and later -- vector spaces have been recapped earlier in section 1.4:
\begin{labeledquote}\sf\label{q:topvs}
\textbf{1.6 Topological vector spaces} Suppose $\tau$ is a topology on a vector space $X$
......@@ -241,16 +241,16 @@ do not add new knowledge or new results, but aggregate and organize the already
ones, possibly reformulating them for a more uniform exposition. But still, one can
distinguish recap parts -- as the ones above -- which are much more telegraphic in nature
from the primary material presented in the textbook.
\end{newpart}
\end{example}
\subsection{Common Ground in Formal Mathematics}
Where applicable, common ground in formal mathematics is typical established via direct
Where applicable, common ground in formal mathematics is typically established via direct
imports of symbols, theorems, notations, etc. Formal documents emphasize correctness and
do not focus on human readability so they do not re-introduce concepts or provide,
verbalizations of definitions.
For instance, In Isabelle and Coq knowledge is organized \emph{Theories} and
For instance, In Isabelle and Coq knowledge is organized in \emph{Theories} and
\emph{Modules} which are effectively named sets of declarations. The incremental
development process is enabled via the \textsc{imports} and, respectively, \textsc{Require
Import} statements that effectively opens a library module by name and enables its
......@@ -267,7 +267,7 @@ ground section.
The notation and terminology used in this paper have been introduced in the
following papers: [4], [11], [12], [19], [9], [3], [5], [6], [21], [22], [1], [2], [7], [18],
[20], [24], [25], [23], [16], [13], [14], [10], [15], and [8].
[\ldots]2
[\ldots]
In this paper $T$ , $U$ are non empty topological spaces, $t$ is a point of $T$ , and
$n$ is a natural number.
\end{labeledquote}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment