diff --git a/doc/report/intro.tex b/doc/report/intro.tex index 8f32547465ed30a8ed4515570ef39b66fd9fca62..a54ffb27b5b53735b6e2ba3a517c9aa2220baaaf 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 54ff2c9472776e4fa5b58ae1402082fd8dd792e9..4063e9eb8f11fd6fecaff41469843bbfa75edaf5 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},