diff --git a/doc/report/applications-ulo-table.tex b/doc/report/applications-ulo-table.tex
index debbe3cb148abed535cc0d10cdde38b59193e828..485134e6146eae81923af6e2d8bc893c648dcaff 100644
--- a/doc/report/applications-ulo-table.tex
+++ b/doc/report/applications-ulo-table.tex
@@ -2,96 +2,104 @@
\centering
\small
\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}
+ \begin{flushleft}
+ \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}
+ \end{flushleft}
\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}
+ \begin{flushleft}
+ \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}
+ \end{flushleft}
\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}
+ \begin{flushleft}
+ \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}
+ \end{flushleft}
\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}
+ \begin{flushleft}
+ \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}
+ \end{flushleft}
\caption{ULO predicates \emph{not} used in the Coq exports.}\label{fig:used}
\end{subfigure}
\vspace{0.5cm}
diff --git a/doc/report/applications.tex b/doc/report/applications.tex
index 24f29dd50f8e9796a91eef54348f0215271b33ff..287b3ec3e49efd698e9b903df1d3c066a272e29c 100644
--- a/doc/report/applications.tex
+++ b/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 .
}
diff --git a/doc/report/intro.tex b/doc/report/intro.tex
index 3b36c5506b868780b36933c474bfb8ae367d66d1..fcbf4ce6a38a281bf056d1f7c2e5764066c3d372 100644
--- a/doc/report/intro.tex
+++ b/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
diff --git a/doc/report/references.bib b/doc/report/references.bib
index 7c41bfb0a1d48ce7988953909b6abf130a33ca1b..19cd42f612bb86e8e52eeac0ec2ccccb743e08cd 100644
--- a/doc/report/references.bib
+++ b/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}
+}