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

report: report on statistics application

parent 4506a587
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
doc/report/applications-ulo-table.tex
+ 98
− 9
View file @ 3b95f351
\begin{table}[]
\begin{figure}
\centering
\small
\begin{tabularx}{\textwidth}{lll}
\toprule
Predicate & \multicolumn{1}{l}{Use in Isabelle Library} & \multicolumn{1}{l}{Use in Coq Library} \\ \midrule
Timing Simple & 2.7 & 3.0 \\
O3 & 6.0 & 9.0 \\ \bottomrule
\end{tabularx}
\caption{Absolute number of ocurrences of ULO predicates in exports from existing libraries.}\label{tab:gem5diff}
\end{table}
\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}
\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}
\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}
\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}
\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
+ 25
− 7
View file @ 3b95f351
......@@ -4,15 +4,15 @@
With endpoints in place, we can now query the ULO/RDF data set. This
section describes some experiments with the \emph{ulo-endpoint}
Endpoint {API}. In particular, we query the storage backend for some
statistics, implement some quries suggested for tetrapodal search
statistics, implement some queries suggested for tetrapodal search
\subsection{Exploring Existing Data Sets}
As perviously stated, there already exist exports to ULO for both
As previously stated, there already exist exports to ULO for both
Isabelle and Coq libraries~\cite{uloisabelle, ulocoq}. As a very first
application, we simply look at what ULO predicates are actually used
by the respective datasets. Implementing such a query is not very
difficult. In SPARQL, this can be achived with the \texttt{COUNT}
by the respective data sets. Implementing such a query is not very
difficult. In SPARQL, this can be achieved with the \texttt{COUNT}
aggregate.
\begin{lstlisting}
PREFIX ulo: <https://mathhub.info/ulo#>
......@@ -25,12 +25,30 @@ aggregate.
ORDER BY DESC(?count)
\end{lstlisting}
This yields a list of all used predicates with \texttt{?count} being
the number of occurences.
the number of occurrences. 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 results are listed in
figure~\ref{fig:used}. In both cases, the exports use less than a
third of the available predicates.
\input{applications-ulo-table.tex}
We find that both the Isabelle and the Coq data sets only use subsets
of the predicates provided by the ULO ontology. The results are listed in table
We also see that the Isabelle and Coq exports use different
predicates. For example, the Isabelle contains organizational meta
information such as information about paragraphs and sections in the
source document while the Coq export only tells us about the filename
of the Coq source. That is not particularly problematic as long as we
can trace a given object back to the original Isabelle/Coq source.
However, our results do show that both exports have their own
particularities and with more and more third party libraries exported
to ULO one can assume that this heterogeneity only grows. In particular
we want to point to the large number of predicates which remain unused
in both Isabelle and Coq exports. A user formulating queries for ULO
might be oblivious to the fact that only subsets of exports support
given predicates. While not a problem for \emph{ulo-storage} per se,
we expect this to be a major challenge when building a system of
tetrapodal search.
\subsection{Querying for Tetrapodal Search}
......
doc/report/report.tex
+ 1
− 0
View file @ 3b95f351
......@@ -11,6 +11,7 @@
\usepackage{listings}
\usepackage{multicol}
\usepackage{subcaption}
\usepackage{subcaption}
\usepackage{tabularx}
\usepackage{verbatim}
\usepackage[utf8]{inputenc}
......
experimental/ulo/seperate.py
+ 1
− 1
View file @ 3b95f351
......@@ -21,7 +21,7 @@ def shorten_predicate(uri: str) -> str:
uri = uri.replace(ULO_NAMESPACE, 'ulo:')
uri = uri.replace(DCTERMS_NAMESPACE, 'dcterms:')
return uri
return r'\texttt{%s}' % uri
def main():
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment