In defining a group presentation, it is natural to mod out by the subgroup generated by the 'relators', but there is a technical difficulty, this subgroup is not necessarily normal. So we can define it as following:
Let $G$ be a free group on the set $S$, and let $K$ be a subset of $G$. We define the group $\langle S | K \rangle $ as $G/N$, where $N$ is the smallest normal subgroup of $G$ containing $K$.
I quote:
"Unfortunately, it is a theorem of mathematical logic that there is no algorithm which, when given a presentation will find the order of the group. In fact, there is no algorithm to determine whether a given word of $\langle S | K \rangle $ coincides with the identity. Logicians say that the word problem for groups is unsolvable. But although there is no general solution, there are specific cases that can be analyzed, and the following result is very helpful. "
What theorem is that? Where can we find a proof of it?