Skip to content
Snippets Groups Projects
Commit 1f5ccf24 authored by Andreas Schärtl's avatar Andreas Schärtl
Browse files

report: review implementation

parent fe251517
Branches
No related tags found
No related merge requests found
doc/report/figs/screenshot0.png

85.3 KiB

doc/report/figs/screenshot1.png

133 KiB

\begin{figure}
\centering
\begin{subfigure}[b]{0.8\textwidth}
\centering
\shadowbox{\includegraphics[width=\textwidth]{figs/screenshot0.png}}
\caption{Scheduling a new import job in the web interface.}
\end{subfigure}
\vspace{5mm}
\begin{subfigure}[b]{0.8\textwidth}
\centering
\shadowbox{\includegraphics[width=\textwidth]{figs/screenshot1.png}}
\caption{Reviewing a previous import job. This particular job
failed, which illustrates how our web interface presents errors
and logs.}
\end{subfigure}
\caption{The web interface for controlling the Collector and
Importer components. While Collector and Importer can also be
used as library code or with a command line utility, managing
jobs in a web interface is probably the most
convenient.}\label{fig:ss}
\end{figure}
......@@ -6,14 +6,15 @@
\caption{We can think of this tree as visualizing a relation~$R$ where
$(X, Y)~\in~R$ iff there is an edge from~$X$ to~$Y$.}
\end{subfigure}
\hspace{5mm}
\begin{subfigure}[b]{0.4\textwidth}
\centering
\includegraphics[width=\textwidth]{figs/tree-transitive.pdf}
\caption{Transitive closure~$S$ of relation~$R$. Additionally to
each tuple from~$R$ (solid edges), $S$~also contains additional
transitive edges (dotted lines).}
transitive edges (dotted edges).}
\end{subfigure}
\caption{Illustrating the idea behind the transative closure. A
transative closure~$S$ of relation~$R$ is defined as the
\caption{Illustrating the idea behind transitive closures. A
transitive closure~$S$ of relation~$R$ is defined as the
``minimal transitive relation that contains~$R$''~\cite{tc}.}\label{fig:tc}
\end{figure*}
This diff is collapsed.
......@@ -2,12 +2,12 @@
To tackle the vast array of mathematical publications, various ways of
\emph{computerizing} mathematical knowledge have been experimented
with. As it is already difficult for human mathematicians to keep
even a subset of all mathematical knowledge in their mind, a hope is
that computerization will yield great improvement to formal research
by making the results of all collected publications readily available
and easy to search. In literature, this problem is referred to as the
``one brain barrier''~\cite{onebrain}.
with. Already it is difficult for human mathematicians to keep even a
subset of all mathematical knowledge in their mind, a problem referred
to as the ``one brain barrier'' in literature~\cite{onebrain}. A hope
is that computerization will yield great improvement to formal
research by making the results of all collected publications readily
available and easy to search.
One research topic in this field is the idea of a \emph{tetrapodal
search} that combines four distinct areas of mathematical knowledge.
......@@ -24,30 +24,32 @@ structure, tetrapodal search proposes that each kind of mathematical
knowledge should be made available in a storage backend that fits the
kind of data it is providing. With all four areas available for
querying, tetrapodal search intends to then combine the four indexes
into a single query interface. Currently, research is focused on
providing schemas, storage backends and indexes for the four different
kinds of mathematical knowledge. The focus of \emph{ulo-storage} is
the area of organizational knowledge.
into a single query interface. Currently, research aims at providing
schemas, storage backends and indexes for the four different kinds of
mathematical knowledge. In this context, the focus of
\emph{ulo-storage} is the area of organizational knowledge.
A previously proposed way to structure such organizational data is the
A previously proposed way to structure organizational knowledge is the
\emph{upper level ontology} (ULO)~\cite{ulo}. ULO takes the form of an
OWL~ontology~\cite{uloonto} and as such all organization information
is stored as RDF~triplets with a unified schema of
ULO~predicates~\cite{owl}. Some effort has been made to export
existing databases of formal mathematical knowledge to {ULO}. In
existing collections of formal mathematical knowledge to {ULO}. In
particular, exports from Isabelle and Coq-based libraries are
available~\cite{uloisabelle, ulocoq}. The resulting data set is already
quite large, the Isabelle export alone containing more than
available~\cite{uloisabelle, ulocoq}. The resulting data set is
already quite large, the Isabelle export alone containing more than
200~million triplets.
Existing exports from Isabelle and Coq result in a set of XML~files
that contain RDF~triplets. This is a convenient format for exchange
and easily versioned using Git. However, considering the vast number
of triplets, it is impossible to query easily and efficiently in this
state. This is what \emph{ulo-storage} is focused on: Making ULO data
sets accessible for querying and analysis. We collected RDF files
spread over different Git repositories, imported them into a database
and then experimented with APIs for accessing that data set.
and easily tracked using version control systems such as
Git~\cite{gitpaper} as employed by MathHub~\cite{mh}. However,
considering the vast number of triplets, it is impossible to query
easily and efficiently in this state. This is what \emph{ulo-storage}
is focused on: Making ULO data sets accessible for querying and
analysis. We collected RDF files spread over different Git
repositories, imported them into a database and then experimented with
APIs for accessing that data set.
The main contribution of \emph{ulo-storage} is twofold. First, (1)~we
built up various infrastructure components for making organizational
......
......@@ -400,4 +400,23 @@
year = {2009},
urldate = {2020-09-27},
url = {https://www.w3.org/2009/sparql/wiki/Feature:PropertyPaths},
}
\ No newline at end of file
}
@article{gitpaper,
title={GIT--A stupid content tracker},
author={Hamano, Junio C},
journal={Proc. Ottawa Linux Sympo},
volume={1},
pages={385--394},
year={2006},
publisher={Citeseer}
}
@incollection{mh,
title={System description: MathHub. info},
author={Iancu, Mihnea and Jucovschi, Constantin and Kohlhase, Michael and Wiesing, Tom},
booktitle={Intelligent Computer Mathematics},
pages={431--434},
year={2014},
publisher={Springer}
}
......@@ -3,6 +3,7 @@
\usepackage{amsmath}
\usepackage{booktabs}
\usepackage{caption}
\usepackage{fancybox, graphicx}
\usepackage{float}
\usepackage{geometry}
\usepackage{graphicx}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment