diff --git a/doc/report/introduction.tex b/doc/report/introduction.tex index 09831480116364a1c0336df6852ee2f7da40c6c2..e198187f43a2f44adb87dfaf9d550cac6142cf4d 100644 --- a/doc/report/introduction.tex +++ b/doc/report/introduction.tex @@ -13,14 +13,14 @@ One topic of research in this field is the idea of a \emph{tetrapodal search} that combines four distinct areas of mathematical knowledge. These four kinds being (1)~the actual formulae as \emph{symbolic knowledge}, (2)~examples and concrete objects as \emph{concrete - knowledge}, (3)~names and comments as \emph{narrative knowledge} and + knowledge}, (3)~prose, names and comments as \emph{narrative knowledge} and finally (4)~identifiers, references and their relationships, referred to as \emph{organizational knowledge}~\cite{tetra}. Tetrapodal search aims to provide a unified search engine that indexes each of these four different subsets of mathematical knowledge. Because all four kinds of knowledge are inherently unique in their -structure, tetrapodal search proposes that each kind of mathematical +structure, tetrapodal search proposes that each subset of mathematical knowledge should be made available in a storage backend that fits the kind of data it is providing. With all four areas available for querying, tetrapodal search intends to then combine the four indexes @@ -31,8 +31,8 @@ mathematical knowledge. In this context, the focus of A previously proposed way to structure organizational knowledge is the \emph{upper level ontology} (ULO)~\cite{ulo}. ULO takes the form of an -OWL~ontology~\cite{uloonto} and as such all organization information -is stored as RDF~triplets with a unified schema of +OWL~ontology~\cite{uloonto} and as such all organization knowledge is +stored as RDF~triplets with a unified schema of ULO~predicates~\cite{owl}. Some effort has been made to export existing collections of formal mathematical knowledge to {ULO}. In particular, exports from Isabelle and Coq-based libraries are @@ -51,8 +51,8 @@ analysis. We collected RDF files spread over different Git repositories, imported them into a database and then experimented with APIs for accessing that data set. -The main contribution of \emph{ulo-storage} is twofold. First, (1)~we -built up various infrastructure components that make organizational +The contribution of \emph{ulo-storage} is twofold. First, (1)~we built +up various infrastructure components that make organizational knowledge easy to query. These components can make up building blocks of a larger tetrapodal search system. Their design and implementation are discussed in Section~\ref{sec:implementation}. Second, (2)~we ran