diff --git a/doc/report/applications-screenshots.tex b/doc/report/applications-screenshots.tex new file mode 100644 index 0000000000000000000000000000000000000000..65e9c3cb0aa6d39705ef82e79b4f33f997ab74ad --- /dev/null +++ b/doc/report/applications-screenshots.tex @@ -0,0 +1,32 @@ +% https://tex.stackexchange.com/questions/196481/problem-on-subfigure-2x2 + +\begin{figure*} + \centering + \begin{subfigure}[]{0.475\textwidth} + \centering + \shadowbox{\includegraphics[width=\textwidth]{figs/explore1.png}} + \caption{Listing of all contributors in the data set. Clicking + on a given author shows their individual contributions.} + \end{subfigure} + \hfill + \begin{subfigure}[]{0.475\textwidth} + \centering + \shadowbox{\includegraphics[width=\textwidth]{figs/explore2.png}} + \caption{Listing works a given contributor worked on.\\} + \end{subfigure} + \vskip\baselineskip{} + \begin{subfigure}[]{0.475\textwidth} + \centering + \shadowbox{\includegraphics[width=\textwidth]{figs/explore3.png}} + \caption{Examining a single node in the data set. From \texttt{ulo:sourceref} + we can infer the original URI of this object.} + \end{subfigure} + \hfill + \begin{subfigure}[]{0.475\textwidth} + \centering + \shadowbox{\includegraphics[width=\textwidth]{figs/explore4.png}} + \caption{The original source code for a given node in our data set.\\}\label{fig:isrc} + \end{subfigure} + \caption{Exploring the Isabelle~export~\cite{uloisabelle} with a rudimentary + web interface.}\label{fig:appss} +\end{figure*} diff --git a/doc/report/applications.tex b/doc/report/applications.tex index 216003ca69a3fabaf4f0aae18e9cc3e443d41217..b95ba0f2d39b512bd1e6c1aa7f7502a4e3ea74d6 100644 --- a/doc/report/applications.tex +++ b/doc/report/applications.tex @@ -2,7 +2,7 @@ With programming endpoints in place, we can now query the data set containing both Isabelle and Coq exports stored in {GraphDB}. We -experimented with two kinds of applications that talk to a GraphDB +experimented with the following applications that talk to a GraphDB endpoint. \begin{itemize} @@ -11,6 +11,10 @@ endpoint. thirds of existing ULO predicates were not taken advantage of (Section~\ref{sec:expl}). + \item Providing an interactive interface for browsing the data + set. Our implementation is limited to listing basic + information about contributors and their work. + \item We investigated queries that could be used to extend the system into a larger tetrapodal search system. While some organizational queries have obvious canonical solutions others @@ -73,6 +77,44 @@ expect predicates to be evenly distributed in the data set. This is something to keep in mind especially as the number of ULO exports increases. +\subsection{Interactive Exploration} + +Our second application wants to illustrate how to browse an ULO data +set interactively. For this purpose, we developed a web front end that +allows us to browse contributions by author. For this tool, we used +the RDF4J Endpoint, the application itself is implemented in +Java. Figure~\ref{fig:appss} shows four screenshots of the current +version. Once the user has selected a given contribution, we list +some basic information about that object of formal knowledge, such as +type (e.g.\ lemma or corollary) and references to other objects in the +knowledge base. + +\input{applications-screenshots.tex} + +This application is interesting because similar approaches could be +applied when designing IDE~integration for working with organizational +knowledge. Given some object in a document identified by an URI, we +can look at how that object is connected to other objects in the +knowledge graph. We can also connect the dots back to the original +source. In our case, we implemented translation from the +\texttt{ulo:sourceref} predicate as used in the Isabelle +export~\cite{uloisabelle} to the original Isabelle source +(Figure~\ref{fig:isrc}). This is convenient for the user, but required +some extra work for us as application implementors. The reason for +this is that the format of \texttt{ulo:sourceref} is not well-defined, +rather it is up to implementors of library exporters how to format +source references. The consequence is that for each export, developers +of front ends will need to write custom code for finding the original +source. Maybe it would be a reasonable requirement for +\texttt{ulo:sourceref} to have a well-defined format, ideally a +``real'' URI on the open web, if that is applicable for a given +library. + +In summary, while translating from \texttt{ulo:sourceref} to oriental +URI introduced some extra work, implementing this application was easy +and straight-forward. Implementing similar features for other environments +should not be very difficult. + \subsection{Querying for Tetrapodal Search}\label{sec:tetraq} Various queries for a tetrapodal search system were previously diff --git a/doc/report/figs/explore1.png b/doc/report/figs/explore1.png new file mode 100644 index 0000000000000000000000000000000000000000..3c4f331101d3ba4b91c89ca253f807d73d482440 Binary files /dev/null and b/doc/report/figs/explore1.png differ diff --git a/doc/report/figs/explore2.png b/doc/report/figs/explore2.png new file mode 100644 index 0000000000000000000000000000000000000000..45acfc374094b843c95d15d1729aeb0755405d36 Binary files /dev/null and b/doc/report/figs/explore2.png differ diff --git a/doc/report/figs/explore3.png b/doc/report/figs/explore3.png new file mode 100644 index 0000000000000000000000000000000000000000..36fccb34a72ef17f04dbc76aeaecb1c24206fa7c Binary files /dev/null and b/doc/report/figs/explore3.png differ diff --git a/doc/report/figs/explore4.png b/doc/report/figs/explore4.png new file mode 100644 index 0000000000000000000000000000000000000000..4bc367f5bd2568187032c8ac496c1a71476c4f34 Binary files /dev/null and b/doc/report/figs/explore4.png differ diff --git a/doc/report/report.tex b/doc/report/report.tex index 54e57ad8a83dc3cb43ea384b0cb795078a6f27e9..0128957a166ef75ee27fb586897490ccd9fd8de9 100644 --- a/doc/report/report.tex +++ b/doc/report/report.tex @@ -1,7 +1,7 @@ \documentclass[a4paper]{scrartcl} -\usepackage{amsmath} \usepackage[american]{babel} +\usepackage{amsmath} \usepackage{booktabs} \usepackage{caption} \usepackage{fancybox, graphicx} @@ -12,6 +12,7 @@ \usepackage{lipsum} \usepackage{listings} \usepackage{multicol} +\usepackage{mwe} \usepackage{placeins} \usepackage{subcaption} \usepackage{subcaption}