diff --git a/doc/slides/slides.tex b/doc/slides/slides.tex index aa1b84a98cbdbb2146e2473097544e3342c29955..ebf9f798692715e333b561de74b79314b1db2669 100644 --- a/doc/slides/slides.tex +++ b/doc/slides/slides.tex @@ -181,17 +181,38 @@ \mathcal{L} \rightarrow \mathcal{E} \rightarrow \mathcal{D} \end{align*} from \emph{third party library~$\mathcal{L}$} to an \emph{XML - representation~$\mathcal{E}$} to \emph{database storage~$\mathcal{D}$}. - \item When $\mathcal{E}$ changes, so does~$\mathcal{E}$ when a new + export~$\mathcal{E}$} to \emph{database storage~$\mathcal{D}$}. + \item When $\mathcal{L}$ changes, so does~$\mathcal{E}$ when a new export is run. This should result in~$\mathcal{D}$ changing as well. \end{itemize} - \begin{alertblock}{Huh!} - Not trivial! A work around is (1)~re-creating databases from - scratch and (2)~splitting up knowledge into smaller repositories. + \begin{alertblock}{Open Question} + Not trivial! A work around could be (1)~re-creating databases from + scratch and (2)~splitting up knowledge into smaller database + repositories. \end{alertblock} \end{frame} +\begin{frame}{Implementation: Versioning} + \begin{alertblock}{Open Question} + Not trivial! A work around could be (1)~re-creating databases from + scratch and (2)~splitting up knowledge into smaller database + repositories. + \end{alertblock} + + \begin{itemize} + \item Updating existing RDF data sets is unrealistic. Adding + versioning information to~$n$ triplets can add up to + $\mathcal{O}(n)$ triplets. + \item Constantly re-creating the entire data sets introduces + lots of latency between updates. + \item Distributing every given query to a set of smaller + repositories and then joining the result seems like a long term + solution. + \end{itemize} + +\end{frame} + % [Applications & Questions] \section{Exploration} @@ -224,8 +245,8 @@ ULO~predicates. Many predicates are used by neither exports. \end{itemize} - \begin{alertblock}{Huh!} - Queries formulated for a tetrapodal search system have to + \begin{alertblock}{Open Question} + Queries formulated for a tetrapodal search system might have to account for these ``holes'' in existing data sets. \end{alertblock} \end{frame} @@ -247,7 +268,7 @@ \texttt{unimportant} \texttt{universe} \texttt{uses} \end{flushleft} \end{scriptsize} - \caption{Used predicates in an Isabelle export.} + \caption{Used predicates in an Isabelle export~\cite{uloisabelle}.} \end{figure} \begin{figure} @@ -279,10 +300,32 @@ \texttt{uses-implementation} \texttt{uses-interface} \end{flushleft} \end{scriptsize} - \caption{\emph{Unused} predicates in an Isabelle export.} + \caption{Unused predicates in an Isabelle export~\cite{uloisabelle}.} \end{figure} \end{frame} +\subsection{Scoring Items} + +\begin{frame}{Exploration: Scoring} + \begin{itemize} + \item One query for a tetrapodal search system is the following: + ``Find theorems with non-elementary proofs.''~\cite{tetra}. + problems''~\cite{tetra}. + \begin{itemize} + \item Assuming ``elementary'' means easy~\cite{elempro}, we + need to find a way of rating the difficulty of proofs. + \item We can rate proofs by length, check time and so on. + \item Computing metrics can even be formulated in a SPARQL query. + \end{itemize} + \end{itemize} + + \begin{alertblock}{Open Question} + Scanning the entire data set every time we get a tetrapodal query + for a given score is unrealistic. Such queries need to be cached, + either on the organizational or tetrapodal level. + \end{alertblock} +\end{frame} + \subsection{Algorithms and Problems} \begin{frame}{Exploration: Algorithms and Problems} @@ -295,12 +338,15 @@ Tempting but potentially very complicated. \item Algorithms aren't programs! Programs implement algorithms that solve problems. + \item Maybe it would be interesting to collect a database of + algorithms and proofs (OEIS~\cite{oeis} for algorithms). \end{itemize} \end{itemize} - \begin{alertblock}{Huh!} + \begin{alertblock}{Open Question} This illustrates the difficulty in designing an ontology - (schema) that is both expressive and concise. + (schema) that is both expressive and concise. Should an universal + ontology be as concise as possible? \end{alertblock} \end{frame} @@ -320,10 +366,6 @@ subsets of~{ULO}. On the other hand, representing algorithms and algorithmic problems might require us to extend~{ULO}? Maybe instead of tetrapodal search we need $n$-podal search. - \begin{itemize} - \item Maybe it would be interesting to collect a database of - algorithms and proofs (OEIS~\cite{oeis} for algorithms). - \end{itemize} \end{itemize} \end{frame}