From ed7c89a1bf8a5c23820aacb07468511944b60551 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Tue, 16 Jun 2020 17:44:54 +0200
Subject: [PATCH] report: intro: introduce ULO/RDF
---
doc/report/intro.tex | 26 ++++++++++++++++++++++++++
doc/report/references.bib | 8 ++++++++
2 files changed, 34 insertions(+)
diff --git a/doc/report/intro.tex b/doc/report/intro.tex
index 8f32547..a54ffb2 100644
--- a/doc/report/intro.tex
+++ b/doc/report/intro.tex
@@ -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.
diff --git a/doc/report/references.bib b/doc/report/references.bib
index 54ff2c9..4063e9e 100644
--- a/doc/report/references.bib
+++ b/doc/report/references.bib
@@ -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},
--
GitLab