From 8bead541d94c91b49e2ecf1af917cafec0db21e5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Thu, 9 Jul 2020 14:50:29 +0200
Subject: [PATCH] report: add summary about tetra queries
---
doc/report/applications.tex | 19 +++++++++++++++----
1 file changed, 15 insertions(+), 4 deletions(-)
diff --git a/doc/report/applications.tex b/doc/report/applications.tex
index 46ae8d6..5a56ac0 100644
--- a/doc/report/applications.tex
+++ b/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}
--
GitLab