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.

The theory (and practice) of automatic groups is the most generally useful systematic way to deal with these things. There is a nice package written by Derek Holt and his associates called kbmag (available for download here: http://www.warwick.ac.uk/~mareg/download/kbmag2/ ). There is a book "Word Processing in Groups" by Epstein, Cannon, Levy, Holt, Paterson and Thurston that describes the ideas behind this approach. It's not guaranteed to work (not all groups have an "automatic" presentation) but it is surprisingly effective. I made up a short input file for kbmag, and it immediately came back with a "confluent" system of relations (a particular system which has a technical property that when you just do a series of string substitutions you always get the same answer no matter what order you do them in). For your edification, here they are (xi and yi are x^1 and yi^1 respectively, idWord is 1 [edited to show the derivations from kbmag):
#68 eqns; total len: lhs, rhs = 299, 246; 77 states; 0 secs. max len: lhs, rhs = 8, 8. #System is confluent. #Halting with 68 equations. #Exit status is 0 


Let me give a totally useless pureexistence answer, while we wait for someone to show up with a better answer. Namely, if it is true that those relations imply x^{6} = 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 enumerableone 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. 


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! 


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:
To identify the whole group:
In magma, we can do the same operations:
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>." 


It's a bit late answer, but there is a nice proof :). 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 938947. 

