diff --git a/doc/report/applications.tex b/doc/report/applications.tex index 5a56ac055c71cbb6def8373e7eb1696fba012d0b..38e3c7f83d412bcf98f5921de17859688b53484e 100644 --- a/doc/report/applications.tex +++ b/doc/report/applications.tex @@ -273,6 +273,7 @@ existing exports have ``holes''. \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} diff --git a/doc/report/components.tex b/doc/report/components.tex new file mode 100644 index 0000000000000000000000000000000000000000..087c37cad7b52bf90d73f9f88c85ac0491c9f9ea --- /dev/null +++ b/doc/report/components.tex @@ -0,0 +1,63 @@ +\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}. diff --git a/doc/report/references.bib b/doc/report/references.bib index b964641bd71b0fbc6d7f0b4f62fa4c724671287f..8f3b031242b34d0e867e854a0d299fe927b742dc 100644 --- a/doc/report/references.bib +++ b/doc/report/references.bib @@ -188,12 +188,20 @@ } @inproceedings{virt, - title={Virtual theories--a uniform interface to mathematical knowledge bases}, - author={Wiesing, Tom and Kohlhase, Michael and Rabe, Florian}, - booktitle={International Conference on Mathematical Aspects of Computer and Information Sciences}, - pages={243--257}, - year={2017}, - organization={Springer}, - url = {https://kwarc.info/people/frabe/Research/WKR_virtual_17.pdf}, - urldate = {2020-07-09}, -} + title={Virtual theories--a uniform interface to mathematical knowledge bases}, + author={Wiesing, Tom and Kohlhase, Michael and Rabe, Florian}, + booktitle={International Conference on Mathematical Aspects of Computer and Information Sciences}, + pages={243--257}, + year={2017}, + organization={Springer}, + url = {https://kwarc.info/people/frabe/Research/WKR_virtual_17.pdf}, + 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