diff --git a/doc/report/applications.tex b/doc/report/applications.tex index 27a5a9c3b4785afcc57ffa47b36dbe2ee0e8bcab..05604dffd895e7bfc6a688a13ff5e3ff614cafc4 100644 --- a/doc/report/applications.tex +++ b/doc/report/applications.tex @@ -16,9 +16,9 @@ and where other data sources are required. Where possible, we evaluate proof of concept implementations. \begin{itemize} - \item \textbf{$\mathcal{Q}_{1}$ ``Find theorems with non-elementary + \item \textbf{$\mathcal{Q}_1$ ``Find theorems with non-elementary proofs.''} Elementary proofs are those that are considered easy and - obvious. In consequence,~$\mathcal{Q}_{1}$ asks for all proofs + obvious. In consequence,~$\mathcal{Q}_1$ asks for all proofs which are more difficult and not trivial. Of course, just like the distinction between ``theorem'' and ``corollary'' is arbitrary, so is any judgment about whether a proof is elementary or not. @@ -41,7 +41,7 @@ proof of concept implementations. could count the number of words, references and so on to rate the narrative complexity of a proof. This shows that combining symbolic knowledge, narrative knowledge and organizational - knowledge could allow us to service~$\mathcal{Q}_{1}$ in a + knowledge could allow us to service~$\mathcal{Q}_1$ in a heuristic fashion. \textbf{Implementation} Implementing a naive version of the @@ -77,7 +77,7 @@ proof of concept implementations. see that as long as it is based on basic arithmetic, it will be possible to formulate in a SPARQL query. - \item \textbf{$\mathcal{Q}_{2}$ ``Find algorithms that solve + \item \textbf{$\mathcal{Q}_2$ ``Find algorithms that solve $NP$-complete graph problems.''} Here we want the tetrapodal search system to return a listing of algorithms that solve (graph) problems with a given property (runtime complexity). We need @@ -106,7 +106,7 @@ proof of concept implementations. (b)~algorithms that compute a given problem. If ULO had such a concept, we could then introduce new data predicates that tell us something about the properties of problems and - algorithms. Organized in such a schema, query~$\mathcal{Q}_{2}$ + algorithms. Organized in such a schema, query~$\mathcal{Q}_2$ would be easy to service. Of course the question here is whether adding another first level @@ -143,7 +143,7 @@ proof of concept implementations. properties of the generating function) or whether such information can be deduced from symbolic knowledge. - \item \textbf{$\mathcal{Q}_{4}$ ``CAS implementation of Gröbner bases that + \item \textbf{$\mathcal{Q}_4$ ``CAS implementation of Gröbner bases that conform to a definition in AFP.''} Gröbner Bases are a field of study in mathematics particular attractive for use in computer algebra systems (CAS)~\cite{groebner}. This query is asking for @@ -151,7 +151,7 @@ proof of concept implementations. in the Archive of Formal Proofs (AFP). We do have ULO/RDF exports for the AFP~\cite{uloisabelle}. Stated - like this, we can probably assume that $\mathcal{Q}_{4}$ is a query + like this, we can probably assume that $\mathcal{Q}_4$ is a query for a very specific definition, identified by an ULO {URI}. No smart queries necessary. What is missing is the set of implementations, that is symbolic knowledge about actual implementations, and a way @@ -159,7 +159,7 @@ proof of concept implementations. {AFP}. While surely an interesting problem, it is not a task for organizational knowledge. - \item \textbf{$\mathcal{Q}_{5}$ ``All areas of math that {Nicolas G.\ + \item \textbf{$\mathcal{Q}_5$ ``All areas of math that {Nicolas G.\ de Bruijn} has worked in and his main contributions.''} This query is asking by works of a given author~$A$. It also ask for their main contributions, e.g.\ what paragraphs or code~$A$ has authored. @@ -174,7 +174,7 @@ proof of concept implementations. first working version, the exports managed by \emph{ulo-storage} are enough to service this query. - As~$\mathcal{Q}_{5}$ is also asking for the main contributions + As~$\mathcal{Q}_5$ is also asking for the main contributions of~$A$, that is those works that~$A$ authored that are the most important. Importance is a quality measure, simply sorting the result by number of references might be a good start. Again, this @@ -210,7 +210,7 @@ proof of concept implementations. GROUP BY ?work ORDER BY DESC(?refcount) \end{lstlisting} - We see that we can formulate the idea behind~$\mathcal{Q}_{5}$ with + We see that we can formulate the idea behind~$\mathcal{Q}_5$ with one not very complicated SPARQL query. Because here everything is handled by the database access should be quick. \end{itemize}