more

adoptions/intro.tex

 Global mathematical knowledge grows -- at least -- at a rate 120,000 published articles a
-year to a current crop of about 3.5 Million articles.  Even though these are articles are
+year to a current crop of about 3.5 Million articles.  Even though these articles are
 scattered over several thousand journals they -- together with papers in conferences,
 preprints in online or local archives, and talks given in seminars -- function as a
 coherent scientific commons of communal knowledge about the various domains of

adoptions/phenomena.tex

@@ -33,8 +33,6 @@ definition is therefore said to be \emph{quantifier-free}.
  the technical complexity of the definitions.''.
 \end{example}
 
-
-
 \begin{example}{http://arxiv.org/pdf/1502.00978.pdf}\label{ex:calculi}
 \cite{calculi-orig} proves some results about undecidable problems for propositional calculi. 
 In the preliminaries it introduces notations and definitions from scratch:
@@ -188,6 +186,41 @@ where students first encounter the concepts.  \ednote{MK: The solution for this
   transclusion}
 \end{oldpart}
 
+
+\subsection{Common Ground in Formal Mathematics}
+Where applicable, formal mathematical libraries are usually organized in modules representing lists of named declarations  
+
+Where applicable, common ground in formal mathematics is typical 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 \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 declarations to be used in the current development.
+
+\paragraph{Mizar}
+
+In Mizar, formal documents (called \emph{articles}) can be exported as PDF files in a human readable format. The narrative documents 
+contain a part that verbalizes the imports from the source documents and the notation reservations which can be seen as a ``common ground'' section.
+Example \ref{ex:mizar} shows the common ground part for the article on ``Fundamental Group of $n$-sphere for $n \geq 2$'' \cite{topalg_6}.
+
+\begin{example}{http://www.degruyter.com/view/j/forma.2012.20.issue-2/v10037-012-0013-1/v10037-012-0013-1.xml} \label{ex:mizar}
+\begin{labeledquote}
+ 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]
+In this paper $T$ , $U$ are non empty topological spaces, $t$ is a point of $T$ , and
+$n$ is a natural number.
+\end{labeledquote}
+
+
+ 
+\end{example}
+
+
+
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "paper"