diff --git a/doc/report/abstract.tex b/doc/report/abstract.tex index d684a92c00f95ed0ff370d0aac6483443c3480c2..80ea58277d6bff3f4992bed481079aba4cc921cc 100644 --- a/doc/report/abstract.tex +++ b/doc/report/abstract.tex @@ -1,9 +1,12 @@ -Organizational data extracted from mathematical libraries has the -potential to be usable in the design of a universal search engine for -mathematical knowledge. However, it is not enough to only extract this -data into a unified format, it is also necessary to make this information -easily available and queryable. The project \emph{ulo-storage}, which this report -documents, aims to lay out the groundwork. We collect various pieces of -exported data sets into a centralized and efficient store, make that -storage engine available as a publicly available endpoint and then -evaluate different ways of querying that store. +Organizational data extracted from formal libraries has the potential +to be usable in the design of a universal search engine for +mathematical knowledge. However, it is not enough to just extract +formal knowledge into a unified format, it is also necessary that this +information is readily available for querying. \emph{ulo-storage} aims +to lay out the groundwork to do just that. In this project, we +collected various pieces of exported data into a centralized and +efficient store, made that store available as a publicly available +endpoint and then evaluated different ways of querying that +store. Also, implementation of some suggested queries on top of this +system resulted in insight on how a unified format for organizational +mathematical knowledge could be extended. diff --git a/doc/report/applications.tex b/doc/report/applications.tex index 8d9be1334ef2cb7c67efb301c926088612e08c9c..4b8888a8aabb979d07c327c8333faeab670079c5 100644 --- a/doc/report/applications.tex +++ b/doc/report/applications.tex @@ -173,7 +173,7 @@ proof of concept implementations. this should be achieved with ULO/RDF as it contains no unified concept of a sequence. It might be possible to take advantage of \texttt{aligned-with} or some similar concept to find all such - sequences. If this succeeds, an ULO index can provide the first + sequences~\cite{align}. If this succeeds, an ULO index can provide the first step in servicing this query. Here we are in a similar situation as with~$\mathcal{Q}_2$. It is not clear whether we should represent the idea behind ``integer sequences'' as a native @@ -258,3 +258,7 @@ proof of concept implementations. one not very complicated SPARQL query. Because here everything is handled by the database access should be quick. \end{itemize} + +\subsection{Other Queries} + +\emph{{TODO}: SPARQL Queries references in ULO paper} diff --git a/doc/report/references.bib b/doc/report/references.bib index 7a5094ffcf13edc1956585e67f7eceb1c826635b..4a0ec1110f4df2214c7c6b160b156fe820a39052 100644 --- a/doc/report/references.bib +++ b/doc/report/references.bib @@ -128,4 +128,15 @@ author = {Peter Ansell}, urldate = {2020-07-02}, url = {https://github.com/ansell/rdf4j-schema-generator}, -} \ No newline at end of file +} + +@inproceedings{align, + title={Classification of alignments between concepts of formal mathematical systems}, + author={M{\"u}ller, Dennis and Gauthier, Thibault and Kaliszyk, Cezary and Kohlhase, Michael and Rabe, Florian}, + booktitle={International Conference on Intelligent Computer Mathematics}, + pages={83--98}, + year={2017}, + organization={Springer}, + urldate = {2020-07-06}, + url = {https://kwarc.info/people/frabe/Research/GKKMR_alignments_17.pdf}, +}