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

final versions

parent 7f9c9a9c
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 2693 additions and 19 deletions
adoptions/adoptions.zip 0 → 100644
+ 0
− 0
View file @ 24864d4b
File added
adoptions/bibtweaks.sty 0 → 100644
+ 16
− 0
View file @ 24864d4b
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
\iftoggle{bbx:doi}
{\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
{}%
\newunit\newblock
\iftoggle{bbx:eprint}
{\usebibmacro{eprint}}
{}%
\newunit\newblock
\iftoggle{bbx:url}
{\usebibmacro{url+urldate}}
{}}
% LocalWords: renewbibmacro doi eprint iftoggle bbx printfield iffieldundef
adoptions/copyrightLNCS.pdf 0 → 100644
+ 0
− 0
View file @ 24864d4b
File added
adoptions/labeledquote.sty 0 → 100644
+ 11
− 0
View file @ 24864d4b
\newcounter{lquote}
\newsavebox{\lqbox}
\newenvironment{labeledquote}
{\refstepcounter{lquote}
\begin{lrbox}{\lqbox}
\begin{minipage}[t]{\textwidth}
\hfill\begin{minipage}[c]{.8\textwidth}
}
{\end{minipage}\hfill(\arabic{lquote})\end{minipage}
\end{lrbox}
\strut\\[1ex]\noindent\usebox\lqbox\smallskip}
adoptions/llncs.cls 0 → 100644
+ 1210
− 0
View file @ 24864d4b
This diff is collapsed.
adoptions/patterns.tex
+ 17
− 11
View file @ 24864d4b
......@@ -89,6 +89,7 @@ below.
\end{tikzpicture}
\caption{The Architecture of a Realm}\label{fig:realm}\vspace*{-1em}
\end{wrapfigure}
Figure \ref{fig:realm} shows a prototypical realm with $F$ as its interface theory (also
called a \emph{face}) and $n$ pillars each representing a different (yet equivalent)
development of the concepts in the face. Common examples are the different ways to define
......@@ -178,7 +179,7 @@ sub-cases depending on the relation between the recap and cited theory: \emph{eq
recap} (\ref{rc:eq}), \emph{specialization recap} (\ref{rc:sp}) and, in the informal case, \emph{postulated
recap} (\ref{rc:ge}).
Finally, we have the case where the paper builds on several others and has \emph{multiple recaps} (\ref{rc:mr}).
Finally, we have the case where the paper builds on several others and, therefore, has \emph{multiple recaps} (\ref{rc:mr}).
\subsection{Special case: Plain Recaps}\label{rc:pl}
One situation is that of plain recaps where the relation $r$ is an inclusion into the
......@@ -248,11 +249,11 @@ by $v_1$ modulo conservativity.
\begin{center}
\begin{tikzpicture}[xscale=.8]
%realm
\draw[realm] (-2.7,-4.2) rectangle (3.7,2.6) {};
\draw[realm] (-2.7,-4.2) rectangle (3.7,2.2) {};
%p1
\draw[pillar] (-2.5,-3.7) rectangle (1.5,1.8) {};
\draw[pillar] (-2.5,-3.7) rectangle (1.5,1.4) {};
%p2
\draw[pillar] (2.0,-3.7) rectangle (3.5,1.8) {};
\draw[pillar] (2.0,-3.7) rectangle (3.5,1.4) {};
\node (r-name) at (0.7,-4.0) {$\mathit{Realm}$};
\node (p1-name) at (-0.5,-3.5) {$\mathit{Pillar_1}$};
......@@ -271,7 +272,7 @@ by $v_1$ modulo conservativity.
\node[thy] (bot2) at (2.75,-3) {$\bot$};
\node[thy] (r) at (0.7,2.3) {Realm Face};
\node[thy] (r) at (0.7,1.9) {Realm Face};
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
......@@ -637,7 +638,7 @@ exposition on them.
\draw[struct] (f1) -- node[below]{$v_1$} (r1);
\draw[struct] (f2) -- node[below]{$v_2$} (r2);
\end{tikzpicture}
\caption{Publication Graph}
\caption{Publication Graph}\label{fig:multiple-publ}
\end{center}
\end{subfigure}
\qquad
......@@ -662,22 +663,27 @@ exposition on them.
\draw[struct] (f1) -- node[below]{$v_1$} (t);
\draw[struct] (f2) -- node[below]{$v_2$} (t);
\end{tikzpicture}
\caption{Aggregation Graph}
\caption{Aggregation Graph}\label{fig:multiple-aggr}
\end{center}
\end{subfigure}
\caption{Multiple Recaps (Example \ref{ex:rudin})}\label{fig:multiple}
\end{center}
\end{figure}
This is a the situation on the left of Figure~\ref{fig:multiple}; for the aggregation
phase this begs the question where the contribution should be placed. In the recap in
Rudin's book mentioned in Section~\ref{sec:survey} we have separate recaps of vector
This is the situation in Figure~\ref{fig:multiple-publ} inspired by Example \ref{ex:rudin} from Rudin's book.
Note that the two recaps import directly from the faces rather than from a specific pillar or paper.
This is intended and covers the typical case of recaps in textbooks and survey articles. For instance, as mentioned
in Section \ref{sec:survey}, Rudin does not directly cite literature in the recaps, but aggregates the vast
literature in an appendix.
For the aggregation phase the multiple recaps situation begs the question of where the contribution should be placed.
In the recap in example \ref{ex:rudin} we have separate recaps of vector
spaces and topological spaces (\ref{q:topspace}), and we analyze them as theory morphisms
from their respective realms. In this case, there is the realm of topological vector
spaces (\ref{q:topvs}) which imports from both realms, this is the natural place for the
contributions. In the case such a realm does not exist yet, the paper can be used as the
natural starting point for (first pillar of) the realm. Actually, the ``union realm''
concept in Figure~\ref{fig:multiple} is a bit simplified. The contribution of the paper
concept in Figure~\ref{fig:multiple-aggr} is a bit simplified. The contribution of the paper
will usually add some conditions -- like conditions (a) and (b) in (\ref{q:topvs}) -- and
use that for the base theories of the realms. This does not invalidate our claim that
there is always a natural realm -- which may have to be created -- for the contribution of
......
adoptions/pgflibrarytikzmmt.code.tex 0 → 100644
+ 96
− 0
View file @ 24864d4b
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% A TIKZ library for MMT Theory Graphs
% copyright 2014 Michael Kohlhase; Released under the LPPL
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% this library provides some standardized node and arrow styles for formatting MMT graph
% diagrams in tikz. The advantage is that we can classify the arrows and nodes
% symbolically and with the styles in this library achieve a uniform look that helps
% readability.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 1. Theories
% a generic theory
\def\outerthysep{.3mm}
\def\innerthysep{.5mm}
\tikzstyle{thy}=[draw,outer sep=\outerthysep,rounded corners,inner sep=\innerthysep]
% a primitive theory
\tikzstyle{primthy}=[thy,double]
% a theory graph
\tikzstyle{thygraph}=[draw,outer sep=1mm,rounded corners,dashed]
%%% 2. Arrows
%%% 2.1. Arrowtips (only internal)
\usetikzlibrary{arrows}
\newcommand{\@mmtarrowtip}{angle 45}
\newcommand{\@mmtreversearrowtip}{angle 45 reversed}
\newcommand{\@mmtarrowtipepi}{triangle 45}
\newcommand{\@mmtarrowtipmonoright}{right hook}
\newcommand{\@mmtarrowtipmonoleft}{left hook}
\newcommand{\@mmtarrowtippartial}{right to}
\newcommand{\@mmtarrowtippartialleft}{left to}
\newcommand{\@mmtreversearrowtippartial}{right to reversed}
\newcommand{\@mmtreversearrowtippartialleft}{left to reversed}
%%% 2.2 the arrow sstyles in graphs
\usetikzlibrary{decorations,decorations.pathmorphing,decorations.markings}
% any morphism
\tikzstyle{morph}=[-\@mmtarrowtip,thick]
\tikzstyle{mapsto}=[|-\@mmtarrowtip] %| any morphism
% structures
\tikzstyle{struct}=[-\@mmtarrowtip,thick]
% inclusions: regular, partial, and left variants
\tikzstyle{include}=[\@mmtarrowtipmonoright-\@mmtarrowtip,thick]
\tikzstyle{revinclude}=[\@mmtarrowtip-\@mmtarrowtipmonoright,thick]
\tikzstyle{pinclude}=[\@mmtarrowtipmonoright-\@mmtarrowtippartial,thick]
\tikzstyle{includeleft}=[\@mmtarrowtipmonoleft-\@mmtarrowtip,thick]
\tikzstyle{pincludeleft}=[\@mmtarrowtipmonoleft-\@mmtarrowtippartialleft,thick]
% views: regular, mono, partial, and left variants
\tikzstyle{preview}=[decorate,
decoration={coil,aspect=0,amplitude=1pt,
segment length=6pt,
pre=lineto,pre length=3pt,
post=lineto,post length=5pt},
thick]
\tikzstyle{view}=[preview,-\@mmtarrowtip]
\tikzstyle{mview}=[preview,\@mmtarrowtipmonoright-\@mmtarrowtip]
\tikzstyle{pview}=[preview,-\@mmtarrowtippartial]
\tikzstyle{pmview}=[preview,\@mmtarrowtipmonoright-\@mmtarrowtippartial]
\tikzstyle{viewleft}=[preview,-\@mmtarrowtip]
\tikzstyle{mviewleft}=[preview,\@mmtarrowtipmonoleft-\@mmtarrowtip]
\tikzstyle{pviewleft}=[preview,-\@mmtarrowtippartialleft]
\tikzstyle{pmviewleft}=[preview,\@mmtarrowtipmonoleft-\@mmtarrowtippartialleft]
\tikzstyle{adoption}=[preview,thin,double,-\@mmtarrowtip]
% biviews: regular, partial, and left variants
\tikzstyle{biview}=[preview,\@mmtarrowtip-\@mmtarrowtip]
\tikzstyle{pbiview}=[preview,\@mmtreversearrowtippartial-\@mmtarrowtippartial]
\tikzstyle{pbiviewleft}=[preview,\@mmtreversearrowtippartialleft-\@mmtarrowtippartialleft]
% defining views (experimental)
\tikzstyle{defview}=[preview,densely dotted,-\@mmtarrowtip]
% meta-theory inclusion
\tikzstyle{meta}=[dotted,-\@mmtarrowtip,thick]
% conservative extensions (abbreviation)
\tikzstyle{conservative}=[hooks-\@mmtarrowtip,double]
% conservative development
\tikzstyle{conservdev}=[hooks-\@mmtarrowtip,dashed,double]
% antimorphisms as striktthroughs
\tikzset{anti/.style={
decoration={markings, mark=between positions 0.2 and 0.8 step 4mm with {
\draw [thick,-] ++ (-3pt,-3pt) -- (3pt,3pt);}},
postaction={decorate}}}
% parallel markup
\tikzstyle{parallel}=[\@mmtarrowtip-\@mmtarrowtip,dashed]
%%% 3. convenience macros
%%% 3.1 the \mmtthy macro takes three arguments, name, decl, axioms and makes a
% table-like structure
\newcommand\mmtthy[3]{\def\@test{#3}%
\begin{array}{l}\textsf{#1}\\\hline #2\ifx\@test\@empty\else\\\hline #3\fi\end{array}}
%%% 3.2 the \mmtar takes two arguments, some tikz options, and an arrow style. \nmmtar
% is a variant that also has a name on top.
\newcommand\mmtar[2][]{\raisebox{.5ex}{\tikz[#1]{\draw[#2] (0,0) -- (.6,0);}}}
\newcommand\nmmtar[3][]{\raisebox{.4ex}{\tikz[#1]{\draw[#2] (0,0) --
node[above]{\ensuremath{\scriptstyle #3}} (.8,0);}}}
adoptions/thesis.pdf 0 → 100644
+ 0
− 0
View file @ 24864d4b
File added
adoptions/tikzlibrarymmt.code.tex 0 → 100644
+ 1
− 0
View file @ 24864d4b
\input{pgflibrarytikzmmt.code.tex}
flatsearch/bibtweaks.sty 0 → 100644
+ 16
− 0
View file @ 24864d4b
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
\iftoggle{bbx:doi}
{\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
{}%
\newunit\newblock
\iftoggle{bbx:eprint}
{\usebibmacro{eprint}}
{}%
\newunit\newblock
\iftoggle{bbx:url}
{\usebibmacro{url+urldate}}
{}}
% LocalWords: renewbibmacro doi eprint iftoggle bbx printfield iffieldundef
flatsearch/flatsearch.zip 0 → 100644
+ 0
− 0
View file @ 24864d4b
File added
flatsearch/labeledquote.sty 0 → 100644
+ 11
− 0
View file @ 24864d4b
\newcounter{lquote}
\newsavebox{\lqbox}
\newenvironment{labeledquote}
{\refstepcounter{lquote}
\begin{lrbox}{\lqbox}
\begin{minipage}[t]{\textwidth}
\hfill\begin{minipage}[c]{.8\textwidth}
}
{\end{minipage}\hfill(\arabic{lquote})\end{minipage}
\end{lrbox}
\strut\\[1ex]\noindent\usebox\lqbox\smallskip}
flatsearch/libs.tex
+ 2
− 2
View file @ 24864d4b
To better understand the concept of framing in modular libraries, consider the theory
graph \cn{u} in Figure~\ref{fig:elal-graph}. The right side of the graph introduces the
graph \cn{U} in Figure~\ref{fig:elal-graph}. The right side of the graph introduces the
elementary algebraic hierarchy building up algebraic structures step by step up to rings;
the left side contains a construction of integer arithmetics. In this graph, the nodes are
theories\footnote{We have left out the quantifiers for the variables $x$, $y$, and $z$
......@@ -42,7 +42,7 @@ Another important property of {\mmt} is that, as discussed in Section \ref{sec:i
{\mmt} URIs are expressive enough to supply names for all induced statements. In fact, we can already access the induced
statements in Figure~\ref{fig:elal-graph} in \mmt. For example, the
statement $\forall x,y,z : \mathbb{Z}.(x+y)+z = x+(y+z)$ induced by the view $\mathsf{c}$ in \textsf{IntArith} has
the {\mmt} URI \cn{u}?\textsf{IntArith}?\textsf{c}/\textsf{g}/\textsf{assoc}.
the {\mmt} URI \cn{U}?\textsf{IntArith}?\textsf{c}/\textsf{g}/\textsf{assoc}.
Still, for external applications, it is essential to have the induced statements explicitly represented.
\paragraph{Generating Induced Statements}
......
flatsearch/llncs.cls 0 → 100644
+ 1210
− 0
View file @ 24864d4b
This diff is collapsed.
flatsearch/pgflibrarytikzmmt.code.tex 0 → 100644
+ 96
− 0
View file @ 24864d4b
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% A TIKZ library for MMT Theory Graphs
% copyright 2014 Michael Kohlhase; Released under the LPPL
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% this library provides some standardized node and arrow styles for formatting MMT graph
% diagrams in tikz. The advantage is that we can classify the arrows and nodes
% symbolically and with the styles in this library achieve a uniform look that helps
% readability.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 1. Theories
% a generic theory
\def\outerthysep{.3mm}
\def\innerthysep{.5mm}
\tikzstyle{thy}=[draw,outer sep=\outerthysep,rounded corners,inner sep=\innerthysep]
% a primitive theory
\tikzstyle{primthy}=[thy,double]
% a theory graph
\tikzstyle{thygraph}=[draw,outer sep=1mm,rounded corners,dashed]
%%% 2. Arrows
%%% 2.1. Arrowtips (only internal)
\usetikzlibrary{arrows}
\newcommand{\@mmtarrowtip}{angle 45}
\newcommand{\@mmtreversearrowtip}{angle 45 reversed}
\newcommand{\@mmtarrowtipepi}{triangle 45}
\newcommand{\@mmtarrowtipmonoright}{right hook}
\newcommand{\@mmtarrowtipmonoleft}{left hook}
\newcommand{\@mmtarrowtippartial}{right to}
\newcommand{\@mmtarrowtippartialleft}{left to}
\newcommand{\@mmtreversearrowtippartial}{right to reversed}
\newcommand{\@mmtreversearrowtippartialleft}{left to reversed}
%%% 2.2 the arrow sstyles in graphs
\usetikzlibrary{decorations,decorations.pathmorphing,decorations.markings}
% any morphism
\tikzstyle{morph}=[-\@mmtarrowtip,thick]
\tikzstyle{mapsto}=[|-\@mmtarrowtip] %| any morphism
% structures
\tikzstyle{struct}=[-\@mmtarrowtip,thick]
% inclusions: regular, partial, and left variants
\tikzstyle{include}=[\@mmtarrowtipmonoright-\@mmtarrowtip,thick]
\tikzstyle{revinclude}=[\@mmtarrowtip-\@mmtarrowtipmonoright,thick]
\tikzstyle{pinclude}=[\@mmtarrowtipmonoright-\@mmtarrowtippartial,thick]
\tikzstyle{includeleft}=[\@mmtarrowtipmonoleft-\@mmtarrowtip,thick]
\tikzstyle{pincludeleft}=[\@mmtarrowtipmonoleft-\@mmtarrowtippartialleft,thick]
% views: regular, mono, partial, and left variants
\tikzstyle{preview}=[decorate,
decoration={coil,aspect=0,amplitude=1pt,
segment length=6pt,
pre=lineto,pre length=3pt,
post=lineto,post length=5pt},
thick]
\tikzstyle{view}=[preview,-\@mmtarrowtip]
\tikzstyle{mview}=[preview,\@mmtarrowtipmonoright-\@mmtarrowtip]
\tikzstyle{pview}=[preview,-\@mmtarrowtippartial]
\tikzstyle{pmview}=[preview,\@mmtarrowtipmonoright-\@mmtarrowtippartial]
\tikzstyle{viewleft}=[preview,-\@mmtarrowtip]
\tikzstyle{mviewleft}=[preview,\@mmtarrowtipmonoleft-\@mmtarrowtip]
\tikzstyle{pviewleft}=[preview,-\@mmtarrowtippartialleft]
\tikzstyle{pmviewleft}=[preview,\@mmtarrowtipmonoleft-\@mmtarrowtippartialleft]
\tikzstyle{adoption}=[preview,thin,double,-\@mmtarrowtip]
% biviews: regular, partial, and left variants
\tikzstyle{biview}=[preview,\@mmtarrowtip-\@mmtarrowtip]
\tikzstyle{pbiview}=[preview,\@mmtreversearrowtippartial-\@mmtarrowtippartial]
\tikzstyle{pbiviewleft}=[preview,\@mmtreversearrowtippartialleft-\@mmtarrowtippartialleft]
% defining views (experimental)
\tikzstyle{defview}=[preview,densely dotted,-\@mmtarrowtip]
% meta-theory inclusion
\tikzstyle{meta}=[dotted,-\@mmtarrowtip,thick]
% conservative extensions (abbreviation)
\tikzstyle{conservative}=[hooks-\@mmtarrowtip,double]
% conservative development
\tikzstyle{conservdev}=[hooks-\@mmtarrowtip,dashed,double]
% antimorphisms as striktthroughs
\tikzset{anti/.style={
decoration={markings, mark=between positions 0.2 and 0.8 step 4mm with {
\draw [thick,-] ++ (-3pt,-3pt) -- (3pt,3pt);}},
postaction={decorate}}}
% parallel markup
\tikzstyle{parallel}=[\@mmtarrowtip-\@mmtarrowtip,dashed]
%%% 3. convenience macros
%%% 3.1 the \mmtthy macro takes three arguments, name, decl, axioms and makes a
% table-like structure
\newcommand\mmtthy[3]{\def\@test{#3}%
\begin{array}{l}\textsf{#1}\\\hline #2\ifx\@test\@empty\else\\\hline #3\fi\end{array}}
%%% 3.2 the \mmtar takes two arguments, some tikz options, and an arrow style. \nmmtar
% is a variant that also has a name on top.
\newcommand\mmtar[2][]{\raisebox{.5ex}{\tikz[#1]{\draw[#2] (0,0) -- (.6,0);}}}
\newcommand\nmmtar[3][]{\raisebox{.4ex}{\tikz[#1]{\draw[#2] (0,0) --
node[above]{\ensuremath{\scriptstyle #3}} (.8,0);}}}
flatsearch/search.tex
+ 6
− 6
View file @ 24864d4b
......@@ -20,13 +20,13 @@ for:
library from Figure~\ref{fig:elal-graph} we would find the associativity axiom
\textsf{SemiGrp}/\textsf{assoc}, its directly inherited versions in \textsf{Monoid}, to
\textsf{Ring} and in particular the version
\cn{u}?\textsf{IntArith}?\textsf{c}/\textsf{g}/\textsf{assoc}.
\cn{U}?\textsf{IntArith}?\textsf{c}/\textsf{g}/\textsf{assoc}.
\item[Applicable Theorem Search] where universal variables in the index can be
instantiated as well; this was introduced for a non-modular formal library
in~\cite{IKRU:mizar:11}. Here we could search for $3+4=\qvar{R}$ and find the induced
statement \cn{u}?\textsf{IntArith}?\textsf{c}/\textsf{comm} with the substitution $R\mapsto
statement \cn{U}?\textsf{IntArith}?\textsf{c}/\textsf{comm} with the substitution $R\mapsto
4+3$, which allows the user to instantiate the query and obtain the equation $3+4=4+3$
together with the justification \cn{u}?\textsf{IntArith}?\textsf{c}/\textsf{comm} that can
together with the justification \cn{U}?\textsf{IntArith}?\textsf{c}/\textsf{comm} that can
directly be used in a proof.
\end{compactdesc}
......@@ -53,9 +53,9 @@ can directly dereference the {\mmt} URI and thus be used to present the induced
humans want a justification that is more understandable than a {\mmt} URI. Fortunately,
this can be generated from the {\mmt} URI by a simple template-based algorithm.
Let us consider the search result
\cn{u}?\textsf{IntArith}?\textsf{c}/\textsf{g}/\textsf{assoc} from the instantiation search
above, where we take \cn{u} to be \verb|http://cds.omdoc.org/cds/elal|. The first step is to
localize the result in the theory \cn{u}?\textsf{IntArith} with the sentence
\cn{U}?\textsf{IntArith}?\textsf{c}/\textsf{g}/\textsf{assoc} from the instantiation search
above, where we take \cn{U} to be \verb|http://cds.omdoc.org/cds/elal|. The first step is to
localize the result in the theory \cn{U}?\textsf{IntArith} with the sentence
\begin{labeledquote}\label{lq:theory}\sf
Induced statement $\forall x,y,z : \mathbb{Z}.(x+y)+z = x+(y+z)$ found in
\underline{\texttt{http://cds.omdoc.org/cds/elal?IntArith}} (\underline{subst},
......
flatsearch/tikzlibrarymmt.code.tex 0 → 100644
+ 1
− 0
View file @ 24864d4b
\input{pgflibrarytikzmmt.code.tex}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment