From 5ef20475a85182fb0d684b6b02bea9397550b3c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me> Date: Mon, 5 Oct 2020 11:53:45 +0200 Subject: [PATCH] app: document exploration --- doc/report/applications-screenshots.tex | 9 +++--- doc/report/applications.tex | 40 +++++++++++++++++++++++-- 2 files changed, 42 insertions(+), 7 deletions(-) diff --git a/doc/report/applications-screenshots.tex b/doc/report/applications-screenshots.tex index 19d8bf6..d0cf217 100644 --- a/doc/report/applications-screenshots.tex +++ b/doc/report/applications-screenshots.tex @@ -5,13 +5,14 @@ \begin{subfigure}[b]{0.475\textwidth} \centering \shadowbox{\includegraphics[width=\textwidth]{figs/explore1.png}} - \caption{Listing of all contributors in the data set.\\~\\} + \caption{Listing of all contributors in the data set. Clicking + on a given author shows their individual contributions.} \end{subfigure} \hfill \begin{subfigure}[b]{0.475\textwidth} \centering \shadowbox{\includegraphics[width=\textwidth]{figs/explore2.png}} - \caption{Listing works a given contributor worked on.} + \caption{Listing works a given contributor worked on.\\} \end{subfigure} \vskip\baselineskip{} \begin{subfigure}[b]{0.475\textwidth} @@ -24,8 +25,8 @@ \begin{subfigure}[b]{0.475\textwidth} \centering \shadowbox{\includegraphics[width=\textwidth]{figs/explore4.png}} - \caption{The original source code for a given node in our data set.\\} + \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{appss} + web interface.}\label{fig:appss} \end{figure*} diff --git a/doc/report/applications.tex b/doc/report/applications.tex index baf18ad..b95ba0f 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 @@ -75,11 +79,41 @@ increases. \subsection{Interactive Exploration} -How the notes all bend and reach around the treeeeeeeeeeees. +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} -Now how I remember you! +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} -- GitLab