Deriving a relation in a group based on a presentation Suppose I have the group presentation $G=\langle x,y\ |\ x^3=y^5=(yx)^2\rangle$. Now, $G$ is isomorphic to $SL(2,5)$ (see my proof here).  This means the relation $x^6=1$ should hold in $G$.  I was wondering if anyone knows how to derive that simply from the group presentation (not using central extensions, etc.).  Even nicer would be an example of how software (GAP, Magma, Magnus, etc.) could automate that.
 A: OK, here is the derivation, based completely on the amazing information provided by Victor Miller (who I should also thank for letting me know about kbmag).
First, some identities:
(1) From $x^3=xyxy$ we get: (a) $x^2=yxy$; (b) $xyx^{-1}=y^{-1}x$; (c) $x^{-1}yx=xy^{-1}$.
(2) From $y^5=xyxy$ we get: (a) $y^4=xyx$; (b) $x^{-1}y^3=yxy^{-1}$; (c) $y^3x^{-1}=y^{-1}xy$.
(3) From (1a) and (3b) we get $(yxy)(yxy^{-1})=(x^2)(x^{-1}y^3) = xy^3$; so $xy^2xy^{-1}=y^{-1}xy^3$.
(4) From (2b) and (1b) we get $(yxy^{-1})(xyx^{-1}) = (x^{-1}y^3)(y^{-1}x) = x^{-1}y^2x$, so that $yxy^{-1}xy=x^{-1}y^2x^2$.
(5) From (2c) we get $y^2x^{-1}y^{-1}=y^{-2}x$; squaring that yields $y(yx^{-1}yx^{-1})y^{-1}=y^{-2}xy^{-2}x$.  (1c), inverse, squared, shows this is the same as $yx^{-1}y^{-2}xy^{-1}=y^{-2}xy^{-2}x$.
(6) Similar to (5).  From (2c) we get $y^2x^{-1}=y^{-2}xy$; squaring that yields $y^2x^{-1}y^2x^{-1}=y^{-1}(y^{-1}xy^{-1}x)y$.  (1b) squared shows this is the same as $y^2x^{-1}y^2x^{-1}=y^{-1}xy^2x^{-1}y$.
OK, now consider the word $(y^{-1}xy^3)xy^{-1}xy$. From (3) this is $xy^2x(y^{-1}xy^{-1}x)y$, which from (1b) squared is $xy^2x(xy^2x^{-1})y=xy^2x^2y^2x^{-1}y$.
This word can also be written as $y^{-1}xy^2(yxy^{-1}xy)$, which from (4) is $y^{-1}xy^2(x^{-1}y^2x^2)$. So the previous two computations show
$y^2x^2y^2xy^{-1}=x^{-1}(y^{-1}xy^2x^{-1}y)yx^2$
$=x^{-1}y^2x^{-1}y^2(x^{-1}yx)x$ ...... from (6)
$=x^{-1}y^2(x^{-1}y^2x)y^{-1}x$ ....... from (1c)
$=(x^{-1}y^2x)y^{-1}xy^{-2}x$ ......... from (1c) squared
$=xy^{-1}x(y^{-2}xy^{-2}x)$ ........... from (1c) squared
$=xy^{-1}(xyx^{-1})y^{-2}xy^{-1}$ ..... from (5)
$=x(y^{-2}xy^{-2}x)y^{-1}$ .............from (1b)
$=(xyx^{-1})y^{-2}xy^{-2}$ ............ from (5)
$=y^{-1}xy^{-2}xy^{-2}$ ............... from (1b).
So $y^2x^2y^2x^{-1}y=y^{-1}xy^{-2}xy^{-2}$, or $y^2x^2y^2=y^{-1}xy^{-2}xy^{-3}x$. But
$y^{-1}xy^{-2}x(y^{-3}x)=y^{-1}xy^{-2}(xyx^{-1})y^{-1}=y^{-1}x(y^{-3}x)y^{-1}=y^{-1}(xyx^{-1})y^{-2}=y^{-2}xy^{-2}$ (through repeated application of (2b) inverse, and (1b)).
Thus $y^2x^2y^2=y^{-2}xy^{-2}$, or $y^4x^2y^4=x$, and from (2a) we get $xyx^4yx=x$, or $1=yx^4yx=(yxy)x^4=x^6$ (the second follows from $x^3$ being central and the third from (1a)).
Done! 
A: It's a bit late answer, but there is a nice proof :).
Denote $t = x^3 = y^5$, so $t$ is in center of $G$. Add new symbol $u$ and state that it commutes with other symbols and $u^{-30}=t$, so we obtain new group $E$ isomorphic to $Ext(C_{30},G)$. Now denote $a = u^{10}x, b=u^{6}y, c=u^{15}yx$. It is easy to check that $a^3=b^5=c^2=1$ and $bac=u$ in $E$. Denote $Q_1 = u^{-1}ba, Q_2 =u^{-1}ab$. You can check that $Q_1^2 = Q_2^2 = 1$. The next holds:
$$Q_1Q_2 = u^{-2}b(a^2)b = u^{-2}b(u^{-2}bab)b = u^{-4}b^2ab^2 = u^{-4}b^2a(b^{-1})b^3 = $$
$$= u^{-4}b^2a(u^{-2}aba)b^3 = u^{-6}b^2a^2bab^3 = u^{-6}(b^2a^2)b(b^2a^2)^{-1}$$ 
Hence $(Q_1Q_2)^5=u^{-30}=t$. But $(Q_2Q_1)^5 = Q_1(Q_1Q_2)^5Q_1 = t$ so $t^2=(Q_1Q_2)^5(Q_2Q_1)^5=1$ in $E$. Clearly, $t^2=1$ should holds in $G$ too. 
The idea of this proof is from this article: "Scalar operators equal to the product of unitary roots of the identity operator", Yu. S. Samoilenko, D. Yu. Yakymenko, 
Ukrainian Mathematical Journal, November 2012, Volume 64, Issue 6, pp 938-947. 
A: This is a very basic answer to the last part of the question. One can derive the relation $x^6=1$ in gap and magma and even identify the group in this case. As a word of caution, these methods may break down depending on the automation one has in mind.
In gap:
 gap> F:= FreeGroup(2); x:=F.1; y:=F.2;
 <free group on the generators [ f1, f2 ]>
 f1
 f2
 gap> G:= F/[x^3*y^-5,x^-3*(y*x)^2];    
 <fp group on the generators [ f1, f2 ]>
 gap> Order(Subgroup(G,[G.1]));        
 6

To identify the whole group:
gap> Order(G); # note this line is not strictly necessary
120
gap> StructureDescription(G);
"SL(2,5)"

In magma, we can do the same operations:
 > G<x,y>:=Group<x,y|x^3=y^5=(y*x)^2>; 
 > Order(sub<G|x>);
 6
 > Order(G); # again this line is not strictly necessary
 120
 > IdentifyGroup(G);
 <120, 5> 

From here, you look up the group as the 5th group of order 120 in the small group data base (see http://magma.maths.usyd.edu.au/magma/handbook/text/703). In the alternative, you could put in your favorite presentation of $SL(2,5)$ and check that is it also group "<120, 5>." 
A: Let me give a totally useless pure-existence answer, while we wait for someone to show up with a better answer.
Namely, if it is true that those relations imply x6 = 1, then there definitely will be an elementary proof of this, using only the group axioms and the relations.  That is, if it is true, then you can be confident that there is a elementary proof, involving just playing with group elements and equations in that group.
This is a consequence of Goedel's Completeness theorem, which says that every statement true in all models of a first order theory has a proof from that theory. In your case, if those relations imply that identity in all groups, then there will be a first order proof of this from the group axioms.
As for automating such questions, of course the word problem is undecidable, so in general it is impossible to automate the general question of determining whether a given identity is a consequence of a given set of relations. 
But your question is not an instance of the word problem, since you are not asking whether the identity holds, but rather, you claim to know that it holds, and want an elementary proof of that. This problem is in principal computable. The reason is that the set of identities that hold in a given presentation is computably enumerable---one can just search through the collection of all proofs, until the desired proof is found. Again, the completeness theorem ensures that there will be such a proof, and so there is a computable procedure to find it.
I apologize for my useless answer.
