report: review Q1

doc/report/applications-ulo-table.tex

@@ -2,6 +2,7 @@
     \centering
     \small
     \begin{subfigure}[]{0.9\textwidth}
+        \begin{flushleft}
             \texttt{check-time} \texttt{defines} \texttt{definition}
             \texttt{derived} \texttt{experimental}
             \texttt{external-size} \texttt{function}
@@ -12,11 +13,13 @@
             \texttt{specified-in} \texttt{specifies}
             \texttt{statement} \texttt{theory} \texttt{type}
             \texttt{unimportant} \texttt{universe} \texttt{uses}
+        \end{flushleft}
         \caption{ULO predicates used in the Isabelle exports.}\label{fig:used}
     \end{subfigure}
     \vspace{0.5cm}
 
     \begin{subfigure}[]{.9\textwidth}
+        \begin{flushleft}
             \texttt{action-times} \texttt{aligned-with}
             \texttt{alternative-for} \texttt{antonym}
             \texttt{automatically-proved} \texttt{axiom}
@@ -41,11 +44,13 @@
             \texttt{similar-to} \texttt{size-properties}
             \texttt{superseded-by} \texttt{theorem} \texttt{typedec}
             \texttt{uses-implementation} \texttt{uses-interface}
+        \end{flushleft}
         \caption{ULO predicates \emph{not} used in the Isabelle exports.}\label{fig:used}
     \end{subfigure}
     \vspace{0.5cm}
 
     \begin{subfigure}[]{.9\textwidth}
+        \begin{flushleft}
             \texttt{axiom} \texttt{definition}
             \texttt{derived} \texttt{example} \texttt{file}
             \texttt{folder} \texttt{internal-size}
@@ -54,11 +59,13 @@
             \texttt{proposition} \texttt{revision}
             \texttt{statement} \texttt{theory} \texttt{type}
             \texttt{uses}
+        \end{flushleft}
         \caption{ULO predicates used in the Coq exports.}\label{fig:used}
     \end{subfigure}
     \vspace{0.5cm}
 
     \begin{subfigure}[]{.9\textwidth}
+        \begin{flushleft}
             \texttt{action-times} \texttt{aligned-with}
             \texttt{alternative-for} \texttt{antonym}
             \texttt{automatically-proved} \texttt{check-time}
@@ -92,6 +99,7 @@
             \texttt{typedec} \texttt{unimportant}
             \texttt{universe} \texttt{uses-implementation}
             \texttt{uses-interface}
+        \end{flushleft}
         \caption{ULO predicates \emph{not} used in the Coq exports.}\label{fig:used}
     \end{subfigure}
     \vspace{0.5cm}

doc/report/applications.tex

@@ -74,67 +74,71 @@ feels particularly applicable to an ULO data set.
 
 \subsection{Querying for Tetrapodal Search}\label{sec:tetraq}
 
-\emph{ulo-storage} was started with the goal of making organizational
-knowledge available for tetrapodal search. We will first take a look
-at how ULO/RDF performs at this task. Conveniently, various queries
-for a tetrapodal search system were suggested in~\cite{tetra}; we will
-investigate how some of them can be realized with ULO/RDF data sets
-and where other data sources are required. Where possible, we evaluate
-proof of concept implementations.
+Various queries for a tetrapodal search system were previously
+suggested in literature~\cite{tetra}. We investigated how some of them
+can be realized with ULO data sets and where other data sources are
+required. Where possible, we evaluate proof of concept
+implementations.
 
 \begin{itemize}
     \item \textbf{$\mathcal{Q}_1$ ``Find theorems with non-elementary
-    proofs.''}  Elementary proofs are those that are considered easy and
-    obvious. In consequence,~$\mathcal{Q}_1$ asks for all proofs
-    which are more difficult and not trivial. Of course, just like the
-    distinction between ``theorem'' and ``corollary'' is arbitrary, so
-    is any judgment about whether a proof is elementary or not.
+    proofs.''}  Elementary proofs are those that are considered easy
+    and obvious~\cite{elempro}. In consequence,~$\mathcal{Q}_1$ has
+    to search for all proofs which are not trivial. Of course, just
+    like the distinction between ``theorem'' and ``corollary'' is
+    arbitrary, so is any judgment about whether a proof is easy or
+    not.
 
     \textbf{Organizational Aspect} A first working hypothesis might be
     to assume that easy proofs are short. In that case, the size, that
     is the number of bytes to store the proof, is our first indicator
-    of proof complexity. ULO/RDF offers the \texttt{ulo:external-size}
+    of proof complexity. {ULO} offers the \texttt{ulo:external-size}
     predicate which will allow us to sort by file size. Maybe small
     file size also leads to quick check times in proof assistants and
     automatic theorem provers. With this assumption in mind we could
     use the \texttt{ulo:check-time} predicate. Correlating proof
-    complexity with file size allows us to answer this query with
-    organizational data based on {ULO/RDF}.
+    complexity with file size allows us to define one indicator of
+    proof complexity based on organizational knowledge alone.
 
     \textbf{Other Aspects} A tetrapodal search system should probably
     also take symbolic knowledge into account. Based on some kind of
     measure of formula complexity, different proofs could be
     rated. Similarly, with narrative knowledge available to us, we
     could count the number of words, references and so on to rate the
-    narrative complexity of a proof. This shows that combining
-    symbolic knowledge, narrative knowledge and organizational
-    knowledge could allow us to service~$\mathcal{Q}_1$ in a
-    heuristic fashion.
+    narrative complexity of a proof. Combining symbolic knowledge,
+    narrative knowledge and organizational knowledge allows us to
+    find proofs which are probably straight forward.
 
     \textbf{Implementation} Implementing a naive version of the
-    organizational aspect can be as simple as querying for all proofs,
-    ordered by size (or check time).
+    organizational aspect can be as simple as querying for all
+    theorems justified by proofs, ordered by size (or check time).
     \begin{lstlisting}
     PREFIX ulo: <https://mathhub.info/ulo#>
 
-    SELECT ?proof ?size
+    SELECT ?theorem ?proof ?size
     WHERE {
-        ?proof ulo:proof ?o .
+        ?theorem ulo:theorem ?i .
+        ?proof ulo:justifies ?theorem .
+        ?proof ulo:proof ?j .
         ?proof ulo:external-size ?size .
     }
     ORDER BY DESC(?size)
     \end{lstlisting}
     Maybe we want to go one step further and calculate a rating that
-    assigns each proof some numeric value of complexity.  We can
-    achieve this in SPARQL as recent versions support arithmetic
-    as part of the SPARQL specification.
+    assigns each proof some numeric score of complexity based on a
+    number of properties.  We can achieve this in SPARQL as recent
+    versions support arithmetic as part of the SPARQL specification.
     \begin{lstlisting}
     PREFIX ulo: <https://mathhub.info/ulo#>
     PREFIX xsd: <http://www.w3.org/2001/XMLSchema#>
 
-    SELECT ?proof ?size (xsd:float(?size) + xsd:float(?checktime) as ?rating)
+    SELECT ?theorem ?proof ?size (
+        xsd:float(?size) + xsd:float(?checktime) as ?rating
+    )
     WHERE {
-        ?proof ulo:proof ?o .
+        ?theorem ulo:theorem ?i .
+        ?proof ulo:justifies ?theorem .
+        ?proof ulo:proof ?j .
         ?proof ulo:external-size ?size .
         ?proof ulo:check-time ?checktime .
     }

doc/report/intro.tex

@@ -35,13 +35,14 @@ organizational knowledge.
 
 A previously proposed way to structure such organizational data is the
 \emph{upper level ontology} (ULO)~\cite{ulo}. ULO takes the form of an
-OWL~ontology and as such all organization information is stored as
-RDF~triplets with a unified schema of ULO~predicates~\cite{owl}.  Some
-effort has been made to export existing databases of formal
-mathematical knowledge to {ULO}. In particular, there exist exports
-from Isabelle and Coq libraries~\cite{uloisabelle, ulocoq}. The
-resulting data set is already quite large, the Isabelle export alone
-containing more than 200~million triplets.
+OWL~ontology~\cite{uloonto} and as such all organization information
+is stored as RDF~triplets with a unified schema of
+ULO~predicates~\cite{owl}.  Some effort has been made to export
+existing databases of formal mathematical knowledge to {ULO}. In
+particular, there exist exports from Isabelle and Coq
+libraries~\cite{uloisabelle, ulocoq}. The resulting data set is
+already quite large, the Isabelle export alone containing more than
+200~million triplets.
 
 Existing exports from Isabelle and Coq result in single or multiple
 RDF~files. This is a convenient format for exchange and easily

doc/report/references.bib

@@ -171,3 +171,18 @@
   booktitle={RIAO},
   year={2007}
 }
+
+@online{elempro,
+    title = {The Definitive Glossary of Higher Mathematical Jargon},
+    organization = {Math Vault},
+    urldate = {2020-07-07},
+    url = {https://mathvault.ca/math-glossary/#elementary}
+}
+
+@online{uloonto,
+    title = {ulo},
+    organization = {MathHub},
+    date = {2019},
+    urldate = {2020-07-07},
+    url = {https://gl.mathhub.info/ulo/ulo}
+}