Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
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}