applications: formulate thoughts on applications

Next up: Move to report, formalize.

experimental/tetrapodal-applications/applications.txt

 01. Find theorems with non-elementary proofs.
+=========================================================================
+
+- elementary proofs are easy
+
+- just like distinction between *theorem* and *corollary* is
+  arbitrary, it is not really defined what an *elementary* proof
+  really has to be
+
+-> proofs could be rated by `check-time`; nothing in literature really
+   mentions the assumption that elementary proofs are easy to check
+
+-> more of a job of (a) symbolic knowledge (complexity for formulas)
+   and (b) narrative knowledge (count the number of references, count
+   the number of narrative elements, e.g. prose, itself)
+
+- if we think of elementary proofs as proofs that support elementary
+  theorems, i.e. theorems that make up the foundations of lots of
+  other theories, we could look into the number of links for a given
+  object
+
+-> look at *inspired-by*, *alternative-for*
 
 02. Find algorithms that solve NP-complete graph problems.
+=========================================================================
+
+- Here we are looking for algorithms. An algorithm should have a
+  (a) specific purpose and (b) ideally input and output parameters of a given
+  type.
+
+-> algorithms aren't really part of ULO; it might make sense to add the
+  concept of an algorithm to ULO, including input parameters and
+  results (types)
+
+-> a theorem should be able to state that a given algorithm is in a
+   given complexity class (space and time) with a proof associated to
+   it
+
+-> with part of ULO, we could search for algorithms of a given `name`
+
+-> even better, it should be possible to link the algorithm to a given
+   "problem"; "problems" don't really fit with the idea of theorems, they
+   are their own thing (TSP is not a theorem or algorithm, it is a problem
+   for which we can state algorithms and about which we can state theorems)
+
+-> of course at that point we are asking ULO to be an ontology for
+   algorithms as well which might be too far fetched
 
 03. Find integer sequences whose generating function is a rational
     polynomial in sin(x) that has a Maple implementation not affected by
     the bug in module x.
+=========================================================================
+
+- This query is about finding concrete integer sequences with some
+  properties.
+
+-> This is a case where information would be split between many
+   sources.  The `name` of the sequences might be part of the
+   organizational data set.  The generating function is part of
+   symbolic knowledge, the Maple implementation could be part of
+   concrete knowledge.
+
+-> Handling this query would probably start by filtering for all
+   integer sequences. It is not clear how this should be achieved with ULO
+   as certainly there is no unified concept of a sequences.
+
+-> It might be possible to take advantage of `aligned-with` or some
+   similar concept to find all such sequences. If this succeeds, ULO
+   can indeed provide the first step in servicing this query.
+
+-> However, finding concrete algorithms and in particular looking
+   inside of them is not organizational data.
+
+04. CAS implementation of Groebner bases that conform to a definition
+    in AFP.
+=========================================================================
+
+- Gröbner Bases are an idea from mathematics particular attractive for
+  use in computer algebra systems (CAS).
+
+- This query is asking for concrete implementations of Gröbner Bases
+  that match the definition in the Archive of Formal Proofs (AFP).
+
+-> Stated like this, it is reasonable to assume that the user already
+   has a specific definition in mind. First a translation from AFP
+   identifier (whatever that is) to an ULO URI is necessary.
+
+-> Armed with the ULO URI, we would need links to symbolic
+   knowledge/concrete knowledge that implements the given
+   concept. Here, we require explicit links to the organizational data
+   set (tags), something that is probably unreasonable.
+
+-> Automatic matching from symbolic knowledge (definition from AFP) to
+   concrete knowledge (implementations) would be preferable.
+
+05. Find all group representations that are good for X (say a software
+    engineer working on something and doesn't know group theory),
+    maybe "computing with in/finite groups".
+=========================================================================
+
+- Here the query is asking for ideas/concepts/data structures for a
+  given problem X.
+
+-> As previously stated, there currently is no concept of a problem
+   class in ULO (e.g. TSP is a problem) which might be exactly what X
+   is about.
 
-04. CAS implementation of Groebner bases that conform to a
-    definition in AFP.
+-> As a fallback, we could look into narrative knowledge and search
+   for keywords related to X. This would yield certain references we
+   could follow up upon.
 
-05. Find all group representations that are good for X (say a
-    software engineer working on something and doesn't know group
-    theory), maybe ``computing with in/finite groups''.
+-> Group representations I would except as part of symbolic knowledge.
+   With the references either from (a) narrative knowledge (keywords)
+   or (b) from organizational knowledge ULO (URIs), look up the
+   symbolic information with these
 
 06. Math software systems that implement algorithms from MSC48CXX (or
     that compute a particular thing).
+=========================================================================
+
+- Again, this is a question about algorithms A that solve a given
+  problem P. In this case, P is part of some specific resource or
+  publication.
+
+-> ULO should allow us to list all objects in a given resource.
+
+-> If we have a concept of "problems" as discussed before as well as
+   links from algorithms (concrete knowledge) to problems, this query
+   is easy to service.
 
 07. All areas of math that {Nicolas G.\ de Bruijn} has worked in and
     his main contributions.
+=========================================================================
+
+- This is a query that has to be answerable by ULO as it is asking
+  about organizational metadata. In particular it is asking by works
+  of a given author A. It also ask for his main contributions,
+  e.g. what paragraphs of a publications A has authored.
+
+-> While we expected this to be a task for organizational data, it
+   might not be the case. The organizational data is more concerned
+   with the "what" and not so much about the "by who". Indeed the
+   tetrapodal search paper states that it is narrative knowledge which
+   contains names (of theorems, proofs, ...) and comments. Maybe this
+   is where we should look instead.
+
+-> However, as ULO contains things like `file` and `para` (paragraph)
+   maybe it does belong to ULO after all. In this case, ULO should add
+   an `authored-by` property that states that a given object was
+   authored by some authors X,Y,Z...
 
 08. All the researchers that have worked on problem X (where X does not
-    have a good name, maybe connected to ``Go'').
+    have a good name, maybe connected to "Go").
+=========================================================================
+
+- This query is similar to 07 in that it is a lookup from author to
+  their works. What is different is that we don't have a formal
+  identifier for X.
+
+-> Mapping a search term such as "Go" to searchable URIs seems like a
+   job for a narrative index. Armed with these URIs lookup is like
+   described in 07.
 
 09. Areas of mathematics that immediate descendants of X worked on.
+=========================================================================
+
+- Again, this is similar to query 07. The difference is that instead
+  of asking for works authored by X it asks for descendants Y of
+  X. Alternatively it could ask for "all colleagues Y of X" or "all
+  researches Y housed at the same department as X.
+
+-> What we need here is knowledge about the connections between
+   different authors. It is not clear where this information should be
+   situated.
+
+   It isn't symbolic nor concrete knowledge. It should be possible to
+   gain some of this information from narrative knowledge. As for
+   organizational knowledge, ULO doesn't really have an elaborate
+   concept of authors and their relationships. At least information
+   such as "Y is professor at university U or research group R" might
+   make sense in ULO.  However it does feel like a stretch to include
+   this information in ULO which right now is more about the
+   organization of mathematical knowledge and not so much about its
+   historic and "earthly" contexts.
 
 10. All graphs whose order is larger than the publication record of
-    its ``inventor'' (name patron).
+    its "inventor" (name patron).
+=========================================================================
+
+- This query is asking about two things: (a) The number of published
+  works by a given author and (b) graphs constructed by a given
+  author. If we can query both of these factoids, merging them to
+  service the query should not be difficult.
+
+-> With a concept of authorship, it should be easy to count the
+   publications for a given author.
+
+-> Counting all vertices is sufficient to gain the order of a given
+   graph G. Of course, such an operation can be quite time consuming
+   and should be cached as part of the graph as part of the index for
+   concrete knowledge.
 
 11. Integer sequences that grow sub-exponentially.
+=========================================================================
+
+- This query is asking about all integer sequences that have a
+  specific property.
+
+-> Query 03 already focused on what needs to be done to search for
+   integer sequences.
+
+-> The growth of an integer sequence is a property that could be
+   stored explicitly (with an associated proof). Then it is easy to
+   serve this query.
+
+-> If we do not have this property stored explicitly, things get more
+   difficult. One could imagine a heuristic on the first n members of
+   a sequence. But doing this for every query is not feasible. It would
+   need to be computed ahead of time from the given concrete knowledge.
 
 12. Published integer sequences not listed in the OEIS.
+=========================================================================
+
+- This query is asking for a match between two indices, namely our own
+  and the OEIS.
+
+-> If we (a) can extract integer sequences from collected concrete
+   knowledge and symbolic knowledge and (b) have an index of the OEIS, this
+   should not be very difficult.
+
+-> As a starter, it might be sufficient to compare some first n
+   members of a sequence and check whether such a sequence is part of
+   OEIS.
+
+-> Of course, if a sequence is generated by some symbolic formula F,
+   this might proof difficult for various reasons. F might be hard to
+   compute and the representation of the OEIS different from ours.
 
 13. Find all polynomials whose list of coefficients occurs as a
     subsequence of a specific OEIS sequence.
+=========================================================================
+
+- This query is asking about (a) coefficients from polynomials and (b)
+  integer sequences.
+
+-> We've already discussed integer sequences in previous queries.
+
+-> Querying coefficients of polynomials might be tricky. It could be
+   extracted from symbolic knowledge, but easy this is not.
+
+-> One could imagine a particular schema for concrete knowledge that
+   stores specific polynomials. But at that point we are building a dedicated
+   index for polynomials, something that might be out of scope.