Are isomorphisms always constructable? Suppose we are given that two finitely presented groups are isomorphic. Is it possible to construct an isomorphism between them?
More precisely, you are given $G_1=\langle S\rangle\cong G_2$, $S$ a finite generating set. Is it always possible to construct a map $S\rightarrow G_2$ which extends to an isomorphism (and prove that this extends!).
 A: The answer is yes, and it does not depend on the groups having solvable word problem.
The basic idea is very simple. You systematically try all possible assignments $\phi(x) \in G_2$ for $x \in S$. For each such assignment, you attempt to check whether it defines a homomorphism, by checking that the images of the relations of $G_1$ under $\phi$ are correct relations in $G_2$. Even if $G_2$ does not have solvable word problem, if these images are valid relations in $G_2$, then it is possible to verify that fact (although you cannot predict how long it might take to verify them).
Since you don't know how long it will take to verify that a given assignment $\phi(x)$ defines a homomorphism, you try only for a fixed length of time, and if it doesn't work then you proceed to the next assignment. But from time to time you go back and re-run all previously unresolved assignments for twice the time that you did previously. That way you are guaranteed eventually to find all homomorphisms $G_1 \to G_2$.
For each such homomorphism, you try to check whether it is surjective by running Todd-Coxeter coset enumeration on the subgroup $\langle \phi(x) : x \in S \rangle$ of $G_2$ for a fixed time. Again, if this remains unresolved, then you arrange to repeat the process later for twice the previous time. So, if $\phi$ is surjective, then you will eventually prove it.
For each surjection found, you can now search for elements of $G_1$ that map onto the generators of $G_2$, and this time you know they exist, so you might as well carry on until you find them. So now you know what $\phi^{-1}$ must be, but you don't know yet that $\phi$ is injective, so you have to try and check that $\phi^{-1}$ is a surjective homomorphism, which again you do using the run a for a fixed time and try again later approach.
But, if the two groups really are isomorphic, then you will eventually find and verify the isomorphism.
Although this all may sound very impractical, there is an implementation of this algorithm (using the Knuth-Bendix string rewriting procedure to verify relations in the groups) in Magma, and the function is called $\mathtt{SearchForIsomorphism}$.  Of course it has restricted application, but it is very quick at solving some well-known exercises like $\langle x,y \mid x^2=y^3 \rangle \cong \langle a,b \mid aba=bab \rangle$.
