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

report: review abstract

parent 3b301868
No related branches found
No related tags found
No related merge requests found
Organizational data extracted from mathematical libraries has the Organizational data extracted from formal libraries has the potential
potential to be usable in the design of a universal search engine for to be usable in the design of a universal search engine for
mathematical knowledge. However, it is not enough to only extract this mathematical knowledge. However, it is not enough to just extract
data into a unified format, it is also necessary to make this information formal knowledge into a unified format, it is also necessary that this
easily available and queryable. The project \emph{ulo-storage}, which this report information is readily available for querying. \emph{ulo-storage} aims
documents, aims to lay out the groundwork. We collect various pieces of to lay out the groundwork to do just that. In this project, we
exported data sets into a centralized and efficient store, make that collected various pieces of exported data into a centralized and
storage engine available as a publicly available endpoint and then efficient store, made that store available as a publicly available
evaluate different ways of querying that store. 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.
...@@ -173,7 +173,7 @@ proof of concept implementations. ...@@ -173,7 +173,7 @@ proof of concept implementations.
this should be achieved with ULO/RDF as it contains no unified this should be achieved with ULO/RDF as it contains no unified
concept of a sequence. It might be possible to take advantage concept of a sequence. It might be possible to take advantage
of \texttt{aligned-with} or some similar concept to find all such 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 step in servicing this query. Here we are in a similar situation
as with~$\mathcal{Q}_2$. It is not clear whether we should as with~$\mathcal{Q}_2$. It is not clear whether we should
represent the idea behind ``integer sequences'' as a native represent the idea behind ``integer sequences'' as a native
...@@ -258,3 +258,7 @@ proof of concept implementations. ...@@ -258,3 +258,7 @@ proof of concept implementations.
one not very complicated SPARQL query. Because here everything is one not very complicated SPARQL query. Because here everything is
handled by the database access should be quick. handled by the database access should be quick.
\end{itemize} \end{itemize}
\subsection{Other Queries}
\emph{{TODO}: SPARQL Queries references in ULO paper}
...@@ -128,4 +128,15 @@ ...@@ -128,4 +128,15 @@
author = {Peter Ansell}, author = {Peter Ansell},
urldate = {2020-07-02}, urldate = {2020-07-02},
url = {https://github.com/ansell/rdf4j-schema-generator}, 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},
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment