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

more

parent 4a1f9332
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
adoptions/intro.tex
+ 27
− 2
View file @ ac68a740
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
......@@ -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}
adoptions/local.bib 0 → 100644
+ 97
− 0
View file @ ac68a740
%%%%% 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}
}
adoptions/local.sty
+ 1
− 0
View file @ ac68a740
\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}
......
adoptions/patterns.tex
+ 89
− 9
View file @ ac68a740
......@@ -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}
\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);
\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) {};
\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}
......
adoptions/phenomena.tex
+ 95
− 3
View file @ ac68a740
......@@ -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
......
flatsearch/libs.tex
+ 4
− 2
View file @ ac68a740
\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}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment