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

report: intro: introduce ULO/RDF

parent 4203ed45
No related branches found
No related tags found
No related merge requests found
......@@ -24,3 +24,29 @@ kind of mathematical knowledge should be made available in a storage
and index backend that fits exactly with the kind of data it is
storing. With all four areas available for querying, tetrapodal search
wants to then combine the four indexes into a single query interface.
\subsection{Structuring Organizational Knowledge}
As it stands, tetrapodal search is long before any usable prototype
being available yet. Currently the interest is in providing storage
backends and indexes for the four different kinds of mathematical
knowledge. The focus of the project work this report is documenting is
organizational knowledge, that is knowledge concerning itself with
names, namespaces, filenames and so on.
A proposed way to structure such organizational data is the
\emph{upper level ontology} (ULO/RDF)~\cite{ulo}. ULO/RDF takes the
form of an OWL~ontology and as such all organization information is
stored as RDF~triplets with a unified schema of ULO~predicates. Some
effort has been made to export existing databases of formal
mathematical knowledge to {ULO/RDF}. In particular, there exist exports
from Isabelle and Coq libraries~\cite{uloisabelle, ulocoq}. The
resulting data set is already quite big, the Isabelle export containing
more than 200~million triplets.
Existing exports from Isabelle and Coq result in a single or multiple
RDF~files. This is a convenient form for exchange and easily versioned
using Git. However, considering the vast number of triplets, it is
impossible to query easily and efficiently as it is. Ultimately this
is what this project work was focused on: Making ULO/RDF accessible
for querying and analysis.
......@@ -22,6 +22,14 @@
url = {https://gl.mathhub.info/Isabelle}
}
@online{ulocoq,
title = {XML Coq Exports},
organization = {MathHub},
date = {2019},
urldate = {2020-06-16},
url = {https://gl.mathhub.info/Coqxml}
}
@online{sparqlpagination,
title = {Paginating SPARQL results},
author = {Joshua Taylor},
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment