Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
schaertl_andreas
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Container Registry
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
supervision
schaertl_andreas
Commits
7c98b670
Commit
7c98b670
authored
4 years ago
by
Andreas Schärtl
Browse files
Options
Downloads
Patches
Plain Diff
report: simplify subscripts in math mode
parent
26086bb4
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
doc/report/applications.tex
+10
-10
10 additions, 10 deletions
doc/report/applications.tex
with
10 additions
and
10 deletions
doc/report/applications.tex
+
10
−
10
View file @
7c98b670
...
...
@@ -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}
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment