Skip to content
Snippets Groups Projects
Commit 5df1e0aa authored by Andreas Schärtl's avatar Andreas Schärtl
Browse files

report: 4.2: work in feedback from Tom

parent b3183291
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
doc/report/applications-preds.tex
+ 0
− 4
View file @ 5df1e0aa
\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}
doc/report/applications-q1.tex 0 → 100644
+ 50
− 0
View file @ 5df1e0aa
\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}
doc/report/applications-ulo-table.tex deleted 100644 → 0
+ 0
− 108
View file @ b3183291
\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}
doc/report/applications.tex
+ 51
− 46
View file @ 5df1e0aa
......@@ -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.
......
doc/report/references.bib
+ 34
− 1
View file @ 5df1e0aa
......@@ -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}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment