report: add summary about tetra queries

doc/report/applications.tex

@@ -255,10 +255,21 @@ implementations.
     should be quick.
 \end{itemize}
 
-%Finally, ULO provides us with the \texttt{aligned-with} predicate to
-%express equality between concepts~$C_1$ and $C_2$ where $C_1$ and
-%$C_2$ typically originate from different formal
-%libraries~\cite{align}.
+Experimenting with $\mathcal{Q}_1$ to $\mathcal{Q}_3$ provided us with
+some insight into ULO and existing ULO exports. $\mathcal{Q}_1$ shows
+that while there is no formal definition for ``elementary proof'', ULO
+allows us to query for heuristics and calculate a difficulty score for
+proofs and their associated theorems. Query~$\mathcal{Q}_2$ illustrates
+the difficulty in finding universal schemas. It remains an open question
+whether ULO should include algorithms as a first class citizen, as a
+concept based around existing ULO predicates or whether it is a better
+idea to design a dedicated ontology and potentially data store entirely.
+Finally, while we were able to formulate a SPARQL query that should
+take care of most of~$\mathcal{Q}_3$ we found that the existing data sets
+contain very little information about authorship. This underlines
+the observations made in Section~\label{sec:expl}, developers writing
+applications that query ULO storage need to be aware of the fact that
+existing exports have ``holes''.
 
 \subsection{Organizational Queries}\label{sec:miscq}