diff --git a/doc/report/applications-preds.tex b/doc/report/applications-preds.tex
index 43cbcd065e267d27f731d297f1a0328802394e6d..dfd4a0f70ba49d1dbe13496847e40638b870d7dd 100644
--- a/doc/report/applications-preds.tex
+++ b/doc/report/applications-preds.tex
@@ -1,6 +1,3 @@
-\begin{figure}
-\end{figure}
-
\begin{figure}
\centering
\begin{subfigure}[]{0.9\textwidth}
@@ -41,7 +38,6 @@
\texttt{count}. The particular results here are from the core
Coq export~\cite{ulocoqspec}.}\label{fig:preds-result}
\end{subfigure}
- \vspace{0.5cm}
\caption{Querying for the kinds of predicates used in a data set}
\end{figure}
diff --git a/doc/report/applications-q1.tex b/doc/report/applications-q1.tex
new file mode 100644
index 0000000000000000000000000000000000000000..cb8a6345b8aa9615082d68432c7e601233cb3553
--- /dev/null
+++ b/doc/report/applications-q1.tex
@@ -0,0 +1,50 @@
+\begin{figure}
+ \centering
+ \begin{subfigure}[]{0.9\textwidth}
+ \begin{lstlisting}
+ PREFIX ulo: <https://mathhub.info/ulo#>
+
+ SELECT ?theorem ?proof ?size
+ WHERE {
+ ?theorem ulo:theorem ?i .
+ ?proof ulo:justifies ?theorem .
+ ?proof ulo:proof ?j .
+ ?proof ulo:external-size ?size .
+ }
+ ORDER BY DESC(?size)
+ \end{lstlisting}
+
+ \caption{SPARQL query that returns each pair of \texttt{theorem}
+ and one given \texttt{proof}, ordered by the size of \texttt{proof}.}\label{fig:q1short}
+ \end{subfigure}
+ \vspace{0.5cm}
+
+ \begin{subfigure}[]{0.9\textwidth}
+ \begin{lstlisting}
+ PREFIX ulo: <https://mathhub.info/ulo#>
+ PREFIX xsd: <http://www.w3.org/2001/XMLSchema#>
+
+ SELECT ?theorem ?proof ?size (
+ xsd:float(?size) + xsd:float(?checktime) as ?rating
+ )
+ WHERE {
+ ?theorem ulo:theorem ?i .
+ ?proof ulo:justifies ?theorem .
+ ?proof ulo:proof ?j .
+ ?proof ulo:external-size ?size .
+ ?proof ulo:check-time ?checktime .
+ }
+ ORDER BY DESC(?rating)
+ \end{lstlisting}
+
+ \caption{SPARQL query that returns each pair of \texttt{theorem}
+ and one given \texttt{proof} ordered by the sum of size and
+ check time of the given proof. A naive rating such as this one
+ will hardly yield helpful results, but it shows that given some
+ kind of complexity scale, we can rate theorems and their proofs
+ by such a scale.}\label{fig:q1long}
+ \end{subfigure}
+
+ \caption{SPARQL queries for serving the organizational aspect
+ of~$\mathcal{Q}_1$.}\label{fig:q1full}
+\end{figure}
diff --git a/doc/report/applications-ulo-table.tex b/doc/report/applications-ulo-table.tex
deleted file mode 100644
index 485134e6146eae81923af6e2d8bc893c648dcaff..0000000000000000000000000000000000000000
--- a/doc/report/applications-ulo-table.tex
+++ /dev/null
@@ -1,108 +0,0 @@
-\begin{figure}
- \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}
- \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}
- \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}
- \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}
- \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}
-
- \caption{ULO predicates in their usage}\label{fig:used}
-\end{figure}
diff --git a/doc/report/applications.tex b/doc/report/applications.tex
index d1596b4874ae74e8171a6c50fb78e062c82b83fb..2770371dd4317e6855ebfbf370623da9bca06f3e 100644
--- a/doc/report/applications.tex
+++ b/doc/report/applications.tex
@@ -40,8 +40,8 @@ list of all used predicates with \texttt{?count} being the number of
occurrences (Figure~\ref{fig:preds-result}). 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 full results are
-listed in Appendix~\ref{sec:used}. In both cases, what sta ndsndsout is
-that either exports use less than a third of the available predicates.
+listed in Appendix~\ref{sec:used}. In both cases, what stands out is
+that both exports use less than a third of the available predicates.
We also see that the Isabelle and Coq exports use different
predicates. For example, the Isabelle contains organizational meta
@@ -78,15 +78,35 @@ implementations.
\item \textbf{$\mathcal{Q}_1$ ``Find theorems with non-elementary
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.
+ to search for all proofs which are not trivial. Of course, just
+ like nay distinction between ``theorem'' and ``corollary'' is
+ going to be somewhat arbitrary, so is any judgment about whether
+ a proof is easy or not.
+
+ Existing research on proof difficulty is either very broad or
+ specific to one problem. For example, some experiments showed that
+ students and prospective school teachers have problems with
+ notation, term rewriting and required
+ prerequisites~\cite{proofund, proofteach}, none of which seems
+ applicable for grading individual proofs for difficulty. On the
+ other hand, there is research on rating proofs for individual
+ subsets of problems, e.g.\ on the satisfiability of a given CNF
+ formula. A particular example is focused on heuristics for how
+ long a SAT solver will take to find a solution for a
+ given~{CNF}~\cite{proofsat}.
\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} offers the \texttt{ulo:external-size}
+ to assume that elementary 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. This is by no means perfect, as
+ even identical proofs can be represented in different ways that
+ might have vastly different size in bytes. It might be tempting to
+ imagine a unique normal form for each proof, but finding such a
+ normal form might very well be impossible. As it is very difficult
+ to find a generalized definition of proof difficulty, we will
+ accept proof size as a first working hypothesis.
+
+ {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
@@ -103,44 +123,29 @@ implementations.
narrative knowledge and organizational knowledge allows us to
find proofs which are probably straight forward.
+ \input{applications-q1.tex}
+
\textbf{Implementation} Implementing a naive version of the
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 ?theorem ?proof ?size
- WHERE {
- ?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 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 ?theorem ?proof ?size (
- xsd:float(?size) + xsd:float(?checktime) as ?rating
- )
- WHERE {
- ?theorem ulo:theorem ?i .
- ?proof ulo:justifies ?theorem .
- ?proof ulo:proof ?j .
- ?proof ulo:external-size ?size .
- ?proof ulo:check-time ?checktime .
- }
- ORDER BY DESC(?rating)
- \end{lstlisting}
- Finding a reasonable rating is its own topic of research, but we
- see that as long as it is based on basic arithmetic, it will be
- possible to formulate in a SPARQL query.
+ Figure~\ref{fig:q1short} illustrates how this can be achieved with
+ a SPARQL query. Maybe we want to go one step further and
+ calculate a rating that 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; Figure~\ref{fig:q1long} shows an example. Finding
+ a reasonable rating is its own topic of research, but we see that
+ as long as it is based on standard arithmetic, it will be possible
+ to formulate in a SPARQL query.
+
+ The queries in Figure~\ref{fig:q1full} return a list of all
+ theorems and associated proofs, naturally this list is bound to be
+ very long. A suggested way to solve this problem is to introduce
+ some kind of cutoff value for our complexity score. Another potential
+ solution is to only list the first~$n$ results, something a user
+ interface would do anyways. Either way, this is not so much an issue
+ for the organizational storage engine and more one that a tetrapodal
+ search aggregator has to account for.
\item \textbf{$\mathcal{Q}_2$ ``Find algorithms that solve
$NP$-complete graph problems.''} Here we want the tetrapodal search
@@ -161,7 +166,7 @@ implementations.
\textbf{Organizational Aspect} If we wish to look up properties
about algorithms from organizational knowledge, we first have to
- think about how to represent this information. We propose to
+ think about how to represent this information. We propose two
approaches, one using the existing ULO ontology and one that
recommends extending ULO to nativly support the concept of
algorithms. Both approaches have their distinct trade-offs.
@@ -206,7 +211,7 @@ implementations.
requires above authorship predicates to actually be in use. With
the Isabelle and Coq exports this was hardly the case; running
some experiments we found less than 15 unique contributors and
- creators, raising suspicion that meat data is missing in the
+ creators, raising suspicion that meta data is missing in the
original library files. Regardless, in theory ULO allows us to
query for objects ordered by authors.
diff --git a/doc/report/references.bib b/doc/report/references.bib
index 85c6bb404c531adfb8a891e51278f093db3678d6..4a787fc64c1bc44f4236e5dd93a42b708ad999e9 100644
--- a/doc/report/references.bib
+++ b/doc/report/references.bib
@@ -212,4 +212,37 @@
booktitle = {International Conference on Logic for Programming Artificial Intelligence and Reasoning},
organization = {Springer},
year = {2013}
-}
\ No newline at end of file
+}
+
+@inproceedings{proofund,
+ title={Undergraduate students’ difficulties in proving mathematics},
+ author={Maslahah, FN and Abadi, AM and others},
+ booktitle={Journal of Physics: Conference Series},
+ volume={1320},
+ number={1},
+ pages={012072},
+ year={2019},
+ organization={IOP Publishing}
+}
+
+@article{proofteach,
+ title={Prospective Mathematics Teachers' Difficulties in Doing Proofs and Causes of Their Struggle with Proofs.},
+ author={Doruk, Muhammet and Kaplan, Abdullah},
+ journal={Online Submission},
+ volume={10},
+ number={2},
+ pages={315--328},
+ year={2015},
+ publisher={ERIC}
+}
+
+@inproceedings{proofsat,
+ title={Relating proof complexity measures and practical hardness of SAT},
+ author={J{\"a}rvisalo, Matti and Matsliah, Arie and Nordstr{\"o}m, Jakob and {\v{Z}}ivn{\`y}, Stanislav},
+ booktitle={International Conference on Principles and Practice of Constraint Programming},
+ pages={316--331},
+ year={2012},
+ organization={Springer},
+ url = {https://www.cs.helsinki.fi/u/mjarvisa/papers/jarvisalo-matsliah-nordstrom-zivny.cp12.pdf},
+ urldate = {2020-07-30}
+}