diff --git a/adoptions/intro.tex b/adoptions/intro.tex
index f07242c676d30e7ec5f7c139ae7ba57af63eacda..f22eef8ef6a4ecaaed63b28863f0a3d302acad1d 100644
--- a/adoptions/intro.tex
+++ b/adoptions/intro.tex
@@ -1,4 +1,26 @@
-A central idea behind the OMDoc/OpenMath data model is that all symbols have a home theory
+Mathematical knowledge grows relentlessly and, even though there are several attempts to formalize parts of it, the
+vast majority of mathematics still exists as informal documents.
+
+In formalized mathematics, representation formats based on theory graphs have proven useful as they provide valuable logic-compatible modularity
+and foster reuse. Theories -- sets of symbols and axioms -- serve as modules and theory morphisms -- truth preserving mappings from the (language of the) source
+theory to the target theory -- formalize inheritance and applicability of theorems.
+
+Currently, full formalization requires a complete rewrite of the documents content in a specific formal system and is prohibitively costly.
+Moreover, it forces commitment to foundational choices that may be irrelevant. As it is also unnecessary for many applications \ednote{``some''/maybe expand here}
+OMDoc allows content of flexible formality (which we call \emph{flexiformal} content).
+
+In particular, we believe just the modular aspect of a document (internal structure, relation to other documents -- imports, applications) can be already useful.
+Especially since informal mathematical knowledge is inherently modular, and deeply interconnected.
+
+\ednote{put one example here}
+
+In this paper, we focus on the modularity of informal mathematics analyze how it manifests in mathematical documents from the perspective of theory graphs.
+In \ref{sec:prel} we briefly introduce OMDoc and theory graphs. Then, we build our intuitions by looking at some examples in section \ref{sec:pheno}.
+We discuss how to represent them using theory graphs in section \ref{sec:patterns}. Finally, in section \ref{sec:conc} we discuss future work and conclude.
+
+
+\begin{oldpart}
+ A central idea behind the OMDoc/OpenMath data model is that all symbols have a home theory
(the document that introduced the concept; essentially the content dictionary). In the
context of flexiformal\footnote{i.e. formalized to flexible depths; see~\cite{KohKoh:tfndc11} and
~\cite{Kohlhase:tffm13} for a discussion of this notion.} digital libraries, this information design creates a tension
@@ -6,4 +28,7 @@ between usability (which demand standardized content dictionaries) and
flexibility/locality.
\ednote{Expand, discuss the alternatives, discuss multiple theories and
realms~\cite{CarFarKoh:tr13}.}
-
+\end{oldpart}
+
+
+
diff --git a/adoptions/local.bib b/adoptions/local.bib
new file mode 100644
index 0000000000000000000000000000000000000000..ff693ee21eae4740fc12281a27a752eee7191fa4
--- /dev/null
+++ b/adoptions/local.bib
@@ -0,0 +1,97 @@
+%%%%% MNets
+@ARTICLE{mnets-orig,
+ author = {Jeremiah Bartz},
+ title = "{Induced and Complete Multinets}",
+ journal = {ArXiv e-prints},
+archivePrefix = "arXiv",
+ eprint = {1502.02059},
+ primaryClass = "math.AG",
+ keywords = {Mathematics - Algebraic Geometry},
+ year = 2015,
+ month = feb,
+ adsurl = {http://adsabs.harvard.edu/abs/2015arXiv150202059B},
+ adsnote = {Provided by the SAO/NASA Astrophysics Data System}
+}
+
+
+@Article{mnets-ref4,
+ Author = {Michael {Falk} and Sergey {Yuzvinsky}},
+ Title = {{Multinets, resonance varieties, and pencils of plane curves.}},
+ FJournal = {{Compositio Mathematica}},
+ Journal = {{Compos. Math.}},
+ ISSN = {0010-437X; 1570-5846/e},
+ Volume = {143},
+ Number = {4},
+ Pages = {1069--1088},
+ Year = {2007},
+ Publisher = {Cambridge University Press, Cambridge; London Mathematical Society, London},
+ Language = {English},
+ DOI = {10.1112/S001043707002722},
+ MSC2010 = {52C35 14H10 05B30},
+ Zbl = {1122.52009}
+}
+
+@book{mnets-ref10,
+ title={On Finite K-Nets in the Complex Projective Plane},
+ author={Stipins, J. and University of Michigan},
+ isbn={9780549180791},
+ url={http://books.google.de/books?id=MBPI4Zw11PUC},
+ year={2007},
+ publisher={University of Michigan.}
+}
+
+@MISC{mnets-ref12,
+ author = {S. Yuzvinsky},
+ title = {A new bound on the number of special fibers in a pencil of curves},
+ year = {2008}
+}
+
+%%%% Covers
+@MISC{covers-orig,
+ author = {Tapani {Hyttinen} and Kaisa {Kangas}},
+ title = {On model theory of covers of algebraically closed fields},
+ year = {2015}
+}
+
+@MISC{covers-13,
+ author = {Boris {Zilber}},
+ title = {Covers of the multiplicative group of an algebraically closed field of characteristic zero},
+ year = {2003}
+}
+
+@MISC{covers-2,
+ author = {Martin {Bays} and Boris {Zilber}},
+ title = {Covers of Multiplicative Groups of Algebraically Closed Fields of Arbitrary Characteristic},
+ year = {2011}
+}
+
+%%%%% calculi
+@MISC{calculi-orig,
+ author = {Grigoriy {Bokov}}
+ title = {Undecidable problems for propositional calculi with implication},
+ year = 2015
+ }
+
+%%%%%
+@MISC{quant-orig,
+ author = {Christopher {Eagle} and Ilijas {Farah} and Eberhard {Kirchberg},
+and Alessandro {Vignati}},
+ title = {Quantifier elimination in C*-algebras},
+ year = 2015,
+}
+
+@article{quant-fs14,
+year={2014},
+issn={0021-2172},
+journal={Israel Journal of Mathematics},
+volume={201},
+number={1},
+doi={10.1007/s11856-014-1046-7},
+title={Model theory of operator algebras II: model theory},
+url={http://dx.doi.org/10.1007/s11856-014-1046-7},
+publisher={The Hebrew University Magnes Press},
+author={Farah, Ilijas and Hart, Bradd and Sherman, David},
+pages={477-505},
+language={English}
+}
+
diff --git a/adoptions/local.sty b/adoptions/local.sty
index 8be27a1289f1b8b20a78c9d66087e2d0751047fe..dc4204ccacff1c035759e16c63d497ac801c711d 100644
--- a/adoptions/local.sty
+++ b/adoptions/local.sty
@@ -1,6 +1,7 @@
\newcommand\mthy[2]{\begin{tabular}{l}\textsf{#1}\\\hline #2\end{tabular}}
\newcommand\cn[1]{\ensuremath{\mathsf{#1}}}
\def\tup#1{\langle #1\rangle}
+\newcommand{\arr}{\rightarrow}
%systems
\newcommand{\mws}{{\scshape{MathWebSearch}}\xspace}
\newcommand{\mmt}{{\scshape{Mmt}}\xspace}
diff --git a/adoptions/patterns.tex b/adoptions/patterns.tex
index ca6ed9724962b815c7d4dc5431aa3893811feff5..5ef4fd833b9a92cf5184e17410994fcb13bf69d8 100644
--- a/adoptions/patterns.tex
+++ b/adoptions/patterns.tex
@@ -9,23 +9,103 @@ I.e. every statement in the paper holds for the original definition too, but not
\begin{figure}[ht]\centering
\begin{tikzpicture}
- \node[thy] (p) at (-2,0) {Paper};
- \node[thy] (l) at (2,0) {Cited Paper};
- \node[thy] (d) at (2,-1) {$\cdots$};
- \node[thy] (b) at (2,-2) {$\bot$};
+ %realm
+ \draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-2.5) rectangle (5,3.5) {};
+ %p-paper
+ \draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
+ %p1
+ \draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-2.5) rectangle (1.5,0.8) {};
+ %p2
+ \draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-2.5) rectangle (4.5,0.8) {};
- \node[thy] (r) at (0,2) {Realm Face};
+ \node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
+ \node (p-name) at (-2,2.6) {$\mathit{Paper}$};
+ \node (p1-name) at (0,0.6) {$\mathit{Pillar_1}$};
+ \node (p2-name) at (4.0,0.6) {$\mathit{Pillar_2}$};
+
+
+ \node[thy] (p) at (-3,0) {Recap};
+ \node[thy] (pc) at (-3,2) {Paper Content};
+
+ \node[thy] (l) at (0.5,0) {Cited Paper};
+ \node[thy] (d) at (0.5,-1) {$\cdots$};
+ \node[thy] (b) at (0.5,-2) {$\bot$};
+
+ \node[thy] (cdots) at (2, -1) {$\cdots$};
+
+
+ \node[thy] (l2) at (3.5,0) {$\top$};
+ \node[thy] (d2) at (3.5,-1) {$\cdots$};
+ \node[thy] (b2) at (3.5,-2) {$\bot$};
+
+
+ \node[thy] (r) at (2,3) {Realm Face};
+
+ \draw[view] (r) to node[above] {$\cn{v}$} (p);
+ \draw[view] (r) to node[left] {$\cn{v_1}$} (l);
+ \draw[view] (r) to node[right] {$\cn{v_2}$} (l2);
- \draw[view] (r) to node[above] {$\cn{v_1}$} (p);
- \draw[view] (r) to node[above] {$\cn{v_2}$} (l);
\draw[include] (l) to (p);
+ \draw[include] (l) to (p);
+ \draw[include] (p) to (pc);
+
\draw[conservative] (b) to (d);
\draw[conservative] (d) to (l);
+ \draw[conservative] (b2) to (d2);
+ \draw[conservative] (d2) to (l2);
+ \draw[view] (b2) to (b);
+ \draw[view] (b) to (b2);
+ \end{tikzpicture}
+\end{figure}
+
+
+\begin{figure}[ht]\centering
+ \begin{tikzpicture}
+ %realm
+ \draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-2.5) rectangle (5,3.5) {};
+ %p-paper
+ \draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
+ %p1
+ \draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-2.5) rectangle (1.5,0.8) {};
+ %p2
+ \draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-2.5) rectangle (4.5,0.8) {};
- \draw (-1,-2.5) -- (3,-2.5) -- (3,2.5) node[above] {Realm} -- (-1,2.5) -- (-1,-2.5);
- \draw (1,-2.5) -- (3,-2.5) -- (3,0.5) node[above] {Pillar} -- (1,0.5) -- (1,-2.5);
+ \node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
+ \node (p-name) at (-2,2.6) {$\mathit{Paper}$};
+ \node (p1-name) at (0,0.6) {$\mathit{Pillar_1}$};
+ \node (p2-name) at (4.0,0.6) {$\mathit{Pillar_2}$};
+ \node[thy] (p) at (-3,0) {Recap};
+ \node[thy] (pc) at (-3,2) {Paper Content};
+
+ \node[thy] (l) at (0.5,0) {Cited Paper};
+ \node[thy] (d) at (0.5,-1) {$\cdots$};
+ \node[thy] (b) at (0.5,-2) {$\bot$};
+
+ \node[thy] (cdots) at (2, -1) {$\cdots$};
+
+
+ \node[thy] (l2) at (3.5,0) {$\top$};
+ \node[thy] (d2) at (3.5,-1) {$\cdots$};
+ \node[thy] (b2) at (3.5,-2) {$\bot$};
+
+
+ \node[thy] (r) at (2,3) {Realm Face};
+
+ \draw[view] (r) to node[left] {$\cn{v_1}$} (l);
+ \draw[view] (r) to node[right] {$\cn{v_2}$} (l2);
+
+ \draw[view] (l) to (p);
+ \draw[view] (p) to (l);
+ \draw[include] (p) to (pc);
+
+ \draw[conservative] (b) to (d);
+ \draw[conservative] (d) to (l);
+ \draw[conservative] (b2) to (d2);
+ \draw[conservative] (d2) to (l2);
+ \draw[view] (b2) to (b);
+ \draw[view] (b) to (b2);
\end{tikzpicture}
\end{figure}
diff --git a/adoptions/phenomena.tex b/adoptions/phenomena.tex
index 5248c133af221b09a876dc9b2ce8f651f5b526c0..52886633cc32c32bc5108c0012db880eca919066 100644
--- a/adoptions/phenomena.tex
+++ b/adoptions/phenomena.tex
@@ -2,16 +2,108 @@
\begin{oldpart}{Examples list}
\begin{itemize}
-\item http://arxiv.org/pdf/1502.01042.pdf uses http://arxiv.org/pdf/math/0401301.pdf with alternative definition
-(similar to ATM case)
\item http://arxiv.org/pdf/1502.01212.pdf
-\item http://arxiv.org/pdf/1502.00978.pdf
\item http://arxiv.org/pdf/1502.02591.pdf
\item http://arxiv.org/pdf/1502.02308.pdf
\item http://arxiv.org/pdf/1502.02413.pdf
\end{itemize}
\end{oldpart}
+\begin{example}[http://arxiv.org/pdf/1502.00573.pdf]
+ \cite{quant-orig} discusses quantifier elimination in $C^*$-algebras and begins by defining the formulas for $C^*$-algebras after the
+ the introduction.
+ \begin{definition}
+ The \emph{formulas} for $C^*$-algebras are recursively defined as follows.
+In each case, $\overline{x}$ denotes a finite tuple of variables (which will later be interpreted as
+elements of a $C^*$-algebra).
+\begin{itemize}
+\item[(1)] If $P(\overline{x})$ is a $*$-polynomial with complex coefficients, then $\|P(\overline{x})\|$ is a formula.
+\item[(2)] If $\varphi_1(\overline{x}), . . . , \varphi_n(\overline{x})$ are formulas and $f : \mathbb{R}^n \arr \mathbb{R}$ is continuous, then
+ $f(\varphi_1(x), . . . , \varphi_n(x))$ is a formula.
+\item[(3)] If $\varphi(\overline{x}, y)$ is a formula and $R \in \mathbb{R}^+$
++, then $\mathrm{sup}_{\|y\| \leq R} \varphi(\overline{x}, y)$ and $\mathrm{inf}_{\|y\| \leq R} \varphi(\overline{x}, y)$
+are formulas.
+\end{itemize}
+We think of $\mathrm{sup}_{\|y\| \leq R}$ and $\mathrm{inf}_{\|y\| \leq R}$ as replacements for the first-order quantifiers
+$\forall$ and $\exists$, respectively. A formula constructed using only clauses (1) and (2) of the
+definition is therefore said to be \emph{quantifier-free}.
+ \end{definition}
+
+ The authors refer to \cite{quant-fs14} for a more complete discussion although it uses a slightly different definition. In fact, the
+ authors explicitly acknowledge that later:
+ ``The definition above is slightly different from the one in \cite{quant-fs14} [...]
+ Since the two versions are equivalent, we have chosen an approach intended to minimize
+ the technical complexity of the definitions.''.
+
+
+\end{example}
+
+
+
+\begin{example}{http://arxiv.org/pdf/1502.00978.pdf}
+\cite{calculi-orig} proves some results about undecidable problems for propositional calculi.
+In the preliminaries it introduces notations and definitions from scratch:
+``Let us consider the language consisting of an infinite set of propositional variables
+$V$ and the signature $\Sigma$, i.e., a finite set of connectives. Letters
+$x, y, z, u, p$ , etc., are used to denote propositional variables.
+Usually connectives are binary or unary such as $\neg, \vee, \wedge,$ or $\arr$.''
+However, it still relies on the literature to fully define the local concepts:
+``Propositional formulas or $\Sigma$-formulas are built up from the signature
+$\Sigma$ and propositional variables $V$ \emph{in the usual way}. '' [emphasis ours]
+
+The paper continues by introducing previous results, by mapping them (implicitly) to the definitions introduced
+locally. For instance :
+\begin{theorem}[Theorem 2.1]
+(Linial and Post, 1949). \textbf{Axm}, \textbf{Ext}, and \textbf{Cmpl} are undecidable for $\textbf{Cl}_{\{\neg, \wedge\}}$.
+\end{theorem}
+where \textbf{Axm}, \textbf{Axm}, \textbf{Ext}, \textbf{Cmpl} and \textbf{Cl} are all defined locally.
+
+Having established local concepts and their properties (via the literature) the paper continues with its contribution.
+\end{example}
+
+
+\begin{example}{http://arxiv.org/pdf/1502.01042.pdf}
+\cite{covers-orig} discusses covers of the multiplicative group of an algebraically closed field which are formally defined in the beginning
+of the paper as follows:
+
+\begin{definition}
+ Let $V$ be a vector space over $Q$ and let $F$ be an algebraically closed field
+of characteristic $0$. A \emph{cover of the multiplicative group} of $F$ is a structure represented by
+an exact sequence
+$0 \arr K \arr V \arr F^∗ \arr 1$ ,
+where the map $V \arr F^*$ is a surjective group homomorphism from $(V, +)$ onto
+$(F^∗, \cdot)$ with kernel $K$. We will call this map \emph{exp}.
+\end{definition}
+
+When, establishing results, \cite{covers-orig} mentions ``Moreover, with an additional axiom (in $L_{\omega_1\omega}$) stating $K \cong Z$, the class is categorical
+in uncountable cardinalities. This was originally proved in \cite{covers-13} but an error was later found
+in the proof and corrected in \cite{covers-2}''.
+
+However, \cite{covers-orig} uses a generalization of the concept in \cite{covers-13} which uses the sequence
+$0 \arr Z \arr C \arr C^* \arr 1$ instead (although later proves some generalizations). Moreover, \cite{covers-2} also
+extends the result in \cite{covers-13} and additionally fixes a hole in the proof mentioned above.
+
+\end{example}
+
+
+\begin{example}{http://arxiv.org/pdf/1502.02059.pdf}
+ \cite{mnets-orig} studies the properties of multinets. In the preliminaries section they are introduced with the following
+ definition:
+ \begin{definition} The union of all completely reducible fibers (with a fixed partition
+into fibers, also called blocks) of a Ceva pencil of degree $d$ is called a $(k, d)-\mathit{multinet}$
+where $k$ is the number of the blocks. The base $X$ of the pencil is determined by the multinet structure and called the base of the multinet.
+ \end{definition}
+
+ Later in that section some properties of multinets are introduced with the phrase ``Several important properties of
+multinets are listed below which have been collected from \cite{mnets-ref4, mnets-ref10, mnets-ref12}.''
+The referenced papers all use slightly different definitions of multinets but they are assumed to be equivalent so that the properties
+hold. In fact, in this paper (\cite{mnets-orig}) the assumption is made explicit -- although not proved -- from the start: ``There are several equivalent ways to
+define multinets. Here we present them using pencils of plane curves.''
+\end{example}
+
+
+
+
\subsection{Recapitulation in Papers}
A common pattern occurs in scientific papers which often have a preliminaries section to
diff --git a/flatsearch/libs.tex b/flatsearch/libs.tex
index 76f4b5fe102d0199f36e84d2f10f67d6ef05e7a6..c32a80ce9e374322f7cde99bfefbf62b6de3cb14 100644
--- a/flatsearch/libs.tex
+++ b/flatsearch/libs.tex
@@ -1,7 +1,9 @@
+\begin{newpart}
Intuitively, the knowledge space of a mathematical library is formed of all the statements that can be proved in it so it
is not possible to (easily) mechanically generate the entire knowledge space.
However, in the context of theory graphs a substantial amount of interesting knowledge can be generated
by leveraging relations between theories (such as imports or theory morphisms).
+\end{newpart}
To better understand the situation in modular libraries, consider the theory graph in
Figure~\ref{fig:elal-graph}. The right side of the graph introduces the elementary
@@ -99,7 +101,7 @@ Note that, since theory flattening preserves theory URIs and doesn't add new axi
new theorems) any view from $S$ to $T$ is also a view from $\overline{S}$ to
$\overline{T}$ so the views in $\overline{\gamma}$ are still valid.
-
+\begin{oldpart}{rewrite this}
An important observation is that the flattening operation for theory graphs is not
idempotent and flattening can be applied repeatedly to a theory graph to generate new
induced symbol declarations. Effectively this generates symbol declarations induced not
@@ -108,7 +110,7 @@ flattened $n$ times will all contain declarations induced by view chains of leng
$n$. Clearly, if there is a view cycle (e.g. $v_1 : S \rightarrow T$ and $v_2 : T
\rightarrow S$) this process can continue indefinitely yielding ever bigger content
libraries.
-
+\end{oldpart}
\paragraph{Induced statements in the {\latin} library}
\ednote{MI@MI: regenerate statistics}