diff --git a/doc/report/applications.tex b/doc/report/applications.tex
index a481fd0dada49da695c23cdcdc8d7c730d82530d..17a2c8c8f9907372c9881f44afc6ccbb0300605d 100644
--- a/doc/report/applications.tex
+++ b/doc/report/applications.tex
@@ -238,15 +238,15 @@ complexity). We need to consider where each of these three components
 might be stored.
 
 \noindent\emph{Symbolic and Concrete Aspects.} First, let us consider
-algorithms. Algorithms can be formulated as computer code which
-can be understood as symbolic knowledge (code represented as a
-syntax tree) or as concrete knowledge (code as text
-files)~\cites[pp. 8--9]{tetra}{virt}. Either way, we will not be
-able to query these indices for what problem a given algorithm is
-solving, nor is it possible to infer properties as complex as
-$NP$-completeness automatically. Metadata of this kind needs to be
-stored in a separate index for organizational knowledge, it being
-the only fit.
+algorithms. Algorithms can be formulated as computer code which can be
+understood as symbolic knowledge (code represented as a syntax tree)
+or as concrete knowledge (code as text
+files)~\cites[pp. 8--9]{tetra}{virt}. Either way, we will not be able
+to query these indices for what problem a given algorithm is solving,
+nor is it possible to infer properties as complex as $NP$-completeness
+automatically in the general case~\cite{np}. Metadata of this kind
+needs to be stored in a separate index for organizational knowledge,
+it being the only fit.
 
 \noindent\emph{Organizational Aspect.} If we wish to look up properties
 about algorithms from organizational knowledge, we first have to
@@ -268,16 +268,17 @@ salesman problem or the sorting problem) in terms of theorems
 (propositions, types) that get implemented by a proof (algorithm,
 program).
 
-As algorithms make up an important part of certain areas of
-research, it might be reasonable to introduce native level support
-for algorithms in ULO or separately in another ontology. An
-argument for adding support directly to ULO is that ULO aims to be
-universal and as such should not be without algorithms. An
-argument for a separate ontology is that what we understand as ULO
-data sets (Isabelle, Coq exports) already contain triplets from
-other ontologies (e.g.\ Dublin Core metadata~\cite{dcreport,
-dcowl}) and keeping concepts separate is not entirely
-unattractive in itself.
+As algorithms make up an important part of certain areas of research,
+it might be reasonable to introduce native level support for
+algorithms in ULO or separately in another ontology. An argument for
+adding support directly to ULO is that ULO aims to be universal and as
+such should not be without algorithms. An argument for a separate
+ontology is that what we understand as ULO data sets (Isabelle, Coq
+exports) already contain predicates from other ontologies
+(e.g.\ Dublin Core metadata~\cite{dcreport, dcowl}). In addition,
+keeping concepts separated in distinct ontologies is not entirely
+unattractive in itself as it can be less overwhelming for a user working
+with these ontologies.
 
 In summary, we see that it is difficult to service~$\mathcal{Q}_2$
 even though the nature of this query is very much one of
@@ -286,7 +287,7 @@ future ULO~exports to find a good way of encoding algorithmic problems
 and solutions. Perhaps a starting point on this endeavor would be to
 find a formal way of structuring information gathered on sites like
 Rosetta Code~\cite{rc}, a site that provides concrete programs that
-solve algorithms problems.
+solve algorithmic problems.
 
 \subsubsection{Contributors and Number of References}
 
diff --git a/doc/report/references.bib b/doc/report/references.bib
index db13ca6f86183ab90a1a1c82b6bfde58a7b97284..7c4e6b822a28a61e3c0b019bd58454075938e487 100644
--- a/doc/report/references.bib
+++ b/doc/report/references.bib
@@ -493,3 +493,10 @@
   year={2004},
   publisher={Springer}
 }
+
+@mastersthesis{np,
+  title={An attempt to automate np-hardness reductions via SO$\exists$ logic},
+  author={Nijjar, Paul},
+  year={2004},
+  school={University of Waterloo}
+}