diff --git a/doc/report/applications-ulo-table.tex b/doc/report/applications-ulo-table.tex
index 915375f5a6387617f6fdee6d36a55072fb0cab0f..debbe3cb148abed535cc0d10cdde38b59193e828 100644
--- a/doc/report/applications-ulo-table.tex
+++ b/doc/report/applications-ulo-table.tex
@@ -1,11 +1,100 @@
-\begin{table}[]
+\begin{figure}
\centering
\small
- \begin{tabularx}{\textwidth}{lll}
- \toprule
- Predicate & \multicolumn{1}{l}{Use in Isabelle Library} & \multicolumn{1}{l}{Use in Coq Library} \\ \midrule
- Timing Simple & 2.7 & 3.0 \\
- O3 & 6.0 & 9.0 \\ \bottomrule
- \end{tabularx}
- \caption{Absolute number of ocurrences of ULO predicates in exports from existing libraries.}\label{tab:gem5diff}
-\end{table}
+ \begin{subfigure}[]{0.9\textwidth}
+ \texttt{check-time} \texttt{defines} \texttt{definition}
+ \texttt{derived} \texttt{experimental}
+ \texttt{external-size} \texttt{function}
+ \texttt{important} \texttt{inductive-on}
+ \texttt{instance-of} \texttt{justifies} \texttt{name}
+ \texttt{para} \texttt{paratype} \texttt{predicate}
+ \texttt{primitive} \texttt{section} \texttt{sourceref}
+ \texttt{specified-in} \texttt{specifies}
+ \texttt{statement} \texttt{theory} \texttt{type}
+ \texttt{unimportant} \texttt{universe} \texttt{uses}
+ \caption{ULO predicates used in the Isabelle exports.}\label{fig:used}
+ \end{subfigure}
+ \vspace{0.5cm}
+
+ \begin{subfigure}[]{.9\textwidth}
+ \texttt{action-times} \texttt{aligned-with}
+ \texttt{alternative-for} \texttt{antonym}
+ \texttt{automatically-proved} \texttt{axiom}
+ \texttt{constructs} \texttt{contains}
+ \texttt{counter-example-for} \texttt{crossrefs}
+ \texttt{declaration} \texttt{deprecated} \texttt{docref}
+ \texttt{example} \texttt{example-for} \texttt{file}
+ \texttt{folder} \texttt{formalizes} \texttt{generated-by}
+ \texttt{hypernym} \texttt{hyponym}
+ \texttt{implementation-uses}
+ \texttt{implementation-uses-implementation-of}
+ \texttt{implementation-uses-interface-of} \texttt{inspired-by}
+ \texttt{inter-statement} \texttt{interface-uses}
+ \texttt{interface-uses-implementation-of}
+ \texttt{interface-uses-interface-of} \texttt{internal-size}
+ \texttt{last-checked-at} \texttt{library}
+ \texttt{library-group} \texttt{logical}
+ \texttt{mutual-block} \texttt{nyms}
+ \texttt{organizational} \texttt{phrase} \texttt{physical}
+ \texttt{proof} \texttt{proposition} \texttt{revision}
+ \texttt{rule} \texttt{same-as} \texttt{see-also}
+ \texttt{similar-to} \texttt{size-properties}
+ \texttt{superseded-by} \texttt{theorem} \texttt{typedec}
+ \texttt{uses-implementation} \texttt{uses-interface}
+ \caption{ULO predicates \emph{not} used in the Isabelle exports.}\label{fig:used}
+ \end{subfigure}
+ \vspace{0.5cm}
+
+ \begin{subfigure}[]{.9\textwidth}
+ \texttt{axiom} \texttt{definition}
+ \texttt{derived} \texttt{example} \texttt{file}
+ \texttt{folder} \texttt{internal-size}
+ \texttt{library} \texttt{library-group}
+ \texttt{predicate} \texttt{primitive}
+ \texttt{proposition} \texttt{revision}
+ \texttt{statement} \texttt{theory} \texttt{type}
+ \texttt{uses}
+ \caption{ULO predicates used in the Coq exports.}\label{fig:used}
+ \end{subfigure}
+ \vspace{0.5cm}
+
+ \begin{subfigure}[]{.9\textwidth}
+ \texttt{action-times} \texttt{aligned-with}
+ \texttt{alternative-for} \texttt{antonym}
+ \texttt{automatically-proved} \texttt{check-time}
+ \texttt{constructs} \texttt{contains}
+ \texttt{counter-example-for} \texttt{crossrefs}
+ \texttt{declaration} \texttt{defines}
+ \texttt{deprecated} \texttt{docref}
+ \texttt{example-for} \texttt{experimental}
+ \texttt{external-size} \texttt{formalizes}
+ \texttt{function} \texttt{generated-by}
+ \texttt{hypernym} \texttt{hyponym}
+ \texttt{implementation-uses}
+ \texttt{implementation-uses-implementation-of}
+ \texttt{implementation-uses-interface-of}
+ \texttt{important} \texttt{inductive-on}
+ \texttt{inspired-by} \texttt{instance-of}
+ \texttt{inter-statement} \texttt{interface-uses}
+ \texttt{interface-uses-implementation-of}
+ \texttt{interface-uses-interface-of}
+ \texttt{justifies} \texttt{last-checked-at}
+ \texttt{logical} \texttt{mutual-block}
+ \texttt{name} \texttt{nyms}
+ \texttt{organizational} \texttt{para}
+ \texttt{paratype} \texttt{phrase}
+ \texttt{physical} \texttt{proof} \texttt{rule}
+ \texttt{same-as} \texttt{section}
+ \texttt{see-also} \texttt{similar-to}
+ \texttt{size-properties} \texttt{sourceref}
+ \texttt{specified-in} \texttt{specifies}
+ \texttt{superseded-by} \texttt{theorem}
+ \texttt{typedec} \texttt{unimportant}
+ \texttt{universe} \texttt{uses-implementation}
+ \texttt{uses-interface}
+ \caption{ULO predicates \emph{not} used in the Coq exports.}\label{fig:used}
+ \end{subfigure}
+ \vspace{0.5cm}
+
+ \caption{ULO predicates in their usage}\label{fig:used}
+\end{figure}
diff --git a/doc/report/applications.tex b/doc/report/applications.tex
index 6559bcc9d70adc5659ca480e1e8a9372019aa07a..09f5a181946f8e338cd23d876b7c6862cc92b213 100644
--- a/doc/report/applications.tex
+++ b/doc/report/applications.tex
@@ -4,15 +4,15 @@
With endpoints in place, we can now query the ULO/RDF data set. This
section describes some experiments with the \emph{ulo-endpoint}
Endpoint {API}. In particular, we query the storage backend for some
-statistics, implement some quries suggested for tetrapodal search
+statistics, implement some queries suggested for tetrapodal search
\subsection{Exploring Existing Data Sets}
-As perviously stated, there already exist exports to ULO for both
+As previously stated, there already exist exports to ULO for both
Isabelle and Coq libraries~\cite{uloisabelle, ulocoq}. As a very first
application, we simply look at what ULO predicates are actually used
-by the respective datasets. Implementing such a query is not very
-difficult. In SPARQL, this can be achived with the \texttt{COUNT}
+by the respective data sets. Implementing such a query is not very
+difficult. In SPARQL, this can be achieved with the \texttt{COUNT}
aggregate.
\begin{lstlisting}
PREFIX ulo: <https://mathhub.info/ulo#>
@@ -25,12 +25,30 @@ aggregate.
ORDER BY DESC(?count)
\end{lstlisting}
This yields a list of all used predicates with \texttt{?count} being
-the number of occurences.
+the number of occurrences. Looking at the results, we find that both
+the Isabelle and the Coq data sets only use subsets of the predicates
+provided by the ULO ontology. The results are listed in
+figure~\ref{fig:used}. In both cases, the exports use less than a
+third of the available predicates.
\input{applications-ulo-table.tex}
-We find that both the Isabelle and the Coq data sets only use subsets
-of the predicates provided by the ULO ontology. The results are listed in table
+We also see that the Isabelle and Coq exports use different
+predicates. For example, the Isabelle contains organizational meta
+information such as information about paragraphs and sections in the
+source document while the Coq export only tells us about the filename
+of the Coq source. That is not particularly problematic as long as we
+can trace a given object back to the original Isabelle/Coq source.
+
+However, our results do show that both exports have their own
+particularities and with more and more third party libraries exported
+to ULO one can assume that this heterogeneity only grows. In particular
+we want to point to the large number of predicates which remain unused
+in both Isabelle and Coq exports. A user formulating queries for ULO
+might be oblivious to the fact that only subsets of exports support
+given predicates. While not a problem for \emph{ulo-storage} per se,
+we expect this to be a major challenge when building a system of
+tetrapodal search.
\subsection{Querying for Tetrapodal Search}
diff --git a/doc/report/report.tex b/doc/report/report.tex
index f56ef813d873a6f25849c52c71bcbbe9a68a3c80..28222aa6f0471c5020b7893d55148aea27c2a891 100644
--- a/doc/report/report.tex
+++ b/doc/report/report.tex
@@ -11,6 +11,7 @@
\usepackage{listings}
\usepackage{multicol}
\usepackage{subcaption}
+\usepackage{subcaption}
\usepackage{tabularx}
\usepackage{verbatim}
\usepackage[utf8]{inputenc}
diff --git a/experimental/ulo/seperate.py b/experimental/ulo/seperate.py
index eff5bc7e6cdc901e1b25a9186dd3a1365cb8cd04..c2148bdbecf490184161766c652d2550f5d87909 100755
--- a/experimental/ulo/seperate.py
+++ b/experimental/ulo/seperate.py
@@ -21,7 +21,7 @@ def shorten_predicate(uri: str) -> str:
uri = uri.replace(ULO_NAMESPACE, 'ulo:')
uri = uri.replace(DCTERMS_NAMESPACE, 'dcterms:')
- return uri
+ return r'\texttt{%s}' % uri
def main():