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

report: add reference to other query paper

But not sure whether I'll follow through with it.
parent 8bead541
No related branches found
No related tags found
No related merge requests found
...@@ -273,6 +273,7 @@ existing exports have ``holes''. ...@@ -273,6 +273,7 @@ existing exports have ``holes''.
\subsection{Organizational Queries}\label{sec:miscq} \subsection{Organizational Queries}\label{sec:miscq}
\emph{{TODO}: SPARQL Queries references in ULO paper} Other organizational queries for organizational data sets have
previously been proposed~\cite{adl}. Here we implement some of them.
\subsection{Experience with Building a Web Frontend}\label{sec:webq} \subsection{Experience with Building a Web Frontend}\label{sec:webq}
\section{Components}\label{sec:components}
With ULO/RDF files in place and available for download on
MathHub~\cite{uloisabelle, ulocoq} as Git repositories, we have the
aim of making the underlying data available for use in applications.
It makes sense to first identify the various components that might
be involved in such a system. They are illustrated in
figure~\ref{fig:components}.
\begin{figure}[]\begin{center}
\includegraphics{figs/components}
\caption{Components involved in the \emph{ulo-storage} system.}\label{fig:components}
\end{center}\end{figure}
\begin{itemize}
\item ULO data is present on various locations, be it Git
repositories, available on web servers or on the local disk.
Regardless where this ULO data is stored, it is the job of a
\emph{Collecter} to assemble these {RDF}~files and forward them
for further processing. This may involve cloning a Git repository or
crawling a file system.
\item With streams of ULO files assembled by the Collecter, this
data then gets passed to an \emph{Importer}. An Importer uploads
received RDF~streams into some kind of permanent storage. For
use in this project, the GraphDB~\cite{graphdb} triplet store was
natural fit.
In this project, both Collecter and Importer ended up being one piece
of software, but this does not have to be the case.
\item Finally, with all triplets stored in a database, an
\emph{Endpoint} is where applications access the underlying
knowledge base. This does not necessarily need to be any specific
software, rather the programming interface of the underlying
database itself could be understood as an endpoint of its
own.
Regardless, some thought can be put into designing an Endpoint as a
layer that lives between application and database that is more
convenient to use than the one provided by the database.
\end{itemize}
These are the components realized for \emph{ulo-storage}. Additionally
to these components, one could think of a \emph{Harvester} component.
We assumed that the ULO triplets are already available in RDF~format.
Indeed for this project this was the case as we work with already
exported triplets from the Isabelle and Coq libraries. However, this
is not necessarily true.
It might be desirable to automate the export from third party formats
to ULO and we think this is what a Harvester should do. It fetches
mathematical knowledge from some remote source and then provides a
volatile stream of ULO data to the Collecter, which then passes it
to the Importer and so on. The big advantage of such an approach would
be that exports from third party libraries can always be up to date
and do not have to be initiated manually. We did not implement a Harvester
for \emph{ulo-storage} but we suggest that it is an idea to keep in mind.
Each component we did implement (Collecter, Importer, Endpoint) will
now be discussed in a separate section. Here we only wanted to give
the reader a general understanding in the infrastructure that makes
up \emph{ulo-storage}.
...@@ -188,12 +188,20 @@ ...@@ -188,12 +188,20 @@
} }
@inproceedings{virt, @inproceedings{virt,
title={Virtual theories--a uniform interface to mathematical knowledge bases}, title={Virtual theories--a uniform interface to mathematical knowledge bases},
author={Wiesing, Tom and Kohlhase, Michael and Rabe, Florian}, author={Wiesing, Tom and Kohlhase, Michael and Rabe, Florian},
booktitle={International Conference on Mathematical Aspects of Computer and Information Sciences}, booktitle={International Conference on Mathematical Aspects of Computer and Information Sciences},
pages={243--257}, pages={243--257},
year={2017}, year={2017},
organization={Springer}, organization={Springer},
url = {https://kwarc.info/people/frabe/Research/WKR_virtual_17.pdf}, url = {https://kwarc.info/people/frabe/Research/WKR_virtual_17.pdf},
urldate = {2020-07-09}, urldate = {2020-07-09},
} }
@inproceedings{adl,
author = {Aspinall, David Denney, Ewen and Lüth Christoph},
title = {A semantic basis for proof queries and transformations},
booktitle = {International Conference on Logic for Programming Artificial Intelligence and Reasoning},
organization = {Springer},
year = {2013}
}
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment