Skip to content
Snippets Groups Projects
Commit 49746b6d authored by Andreas Schärtl's avatar Andreas Schärtl
Browse files

report: applications: elementary can be many things

parent 807c00ca
Branches
No related tags found
No related merge requests found
...@@ -86,8 +86,8 @@ implementations. ...@@ -86,8 +86,8 @@ implementations.
Our first query~$\mathcal{Q}_1$ illustrates how we can compute Our first query~$\mathcal{Q}_1$ illustrates how we can compute
arithmetic scores for some nodes in our knowledge arithmetic scores for some nodes in our knowledge
graph. Query~$\mathcal{Q}_1$ asks us to ``[f]ind theorems with graph. Query~$\mathcal{Q}_1$ asks us to ``[f]ind theorems with
non-elementary proofs.''. Elementary proofs are those that are non-elementary proofs.''. Elementary proofs can be understood as
considered easy and obvious~\cite{elempro}. In those proof that are considered easy and obvious~\cite{elempro}. In
consequence,~$\mathcal{Q}_1$ has to search for all proofs which are consequence,~$\mathcal{Q}_1$ has to search for all proofs which are
not trivial. Of course, just like nay distinction between ``theorem'' not trivial. Of course, just like nay distinction between ``theorem''
and ``corollary'' is going to be somewhat arbitrary, so is any and ``corollary'' is going to be somewhat arbitrary, so is any
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment