Suppose we have a (possibly infinite) group given by generators and relations. One way to prove some inequality is to construct the representation of the group and show inequality in the representation. Is there some other methods?
The most general way is to use the complete presentations. See the book by Sims, for example. The idea is this. Find a presentation of your group as a monoid, that is include inverses of generators in the generating set, include also all relations $aa^{1}=1$. Then use the completion algorithm (called the KnuthBendix procedure) to produce a complete monoid presentation of your group. If you are lucky, the complete presentation will be finite or a least recursive. It will consist of relations $u=v$. Now if you want to check whether a word $w$ is 1 or not, you just apply relations $u=v$ from your complete presentation to $w$ (i.e. replace subword equal to $u$ in $w$ by $v$) until you get a word to which you cannot apply any relation. If that word is empty, $w=1$, if not, $w\ne 1$. Complete recursive presentations exist surprisingly often. For example, many Coxeter groups have them (also see Sims' book mentioned above). Of course, Coxeter groups are residually finite and even linear, so there are other procedures to solve the word problem. But even complicated, nonresidually finite, groups, like the R. Thompson group $F$, have nice recursive complete presentations. 


Following on from Mark's answer, finding an automatic structure for the group is an alternative computational approach to solving this problem, which can work successfully for many groups that do not have finite complete presentations. It is true that all automatic groups have recursive complete presentations, but in general it is very difficult to find such presentations even when they exist, and completeness has been proved to be an undecidable property of a general recursive presentation. The algorithms for computing automatic structures have been implemented, and versions are available in both GAP (as an external package) and Magma. The book "Word Processing in Groups" by David Epstein et al (5 subauthors) is devoted to the general theory of automatic groups. Although not all of out favourite groups are automatic (for example ${\rm SL}_n({\mathbb Z})$ is automatic only when $n=2$, and I believe that it is unknown whether Thompson's group $F$ is automatic), many of them are, including all Coxeter groups, braid groups, and many nonpositively curved groups. If an automatic structure is successfully computed, then the word problem can be solved in at worst quadratic time, finiteness of the group and the orders of elements in the group can be determined, and the growth function of the group can be computed. The programs have been used to help settle genuine open problems about specific finitely presented groups. For example, they were recently used to show that the group $\langle x,y \mid x^3,y^5,(xy)^7,[x,y]^2 \rangle$ is infinite. (There now remain only three quadruples of exponents for which the finiteness of groups with presentations of that type is unknown.) Added later  reply to Mark's query about automaticity implying existence of recursive complete presentation. Thinking about it, I am not certain it is correct without further assumptions on the automatic structure. Let us assume:
Any automatic structure can be replaced by one with uniqueness, but it is unknown whether you can always (simultaneously) achieve subword closure. But all known automatic groups have a structure with these properties, and they hold for socalled shortlex/lenlex structures, in which the wordacceptor language consists of the least representatives of the group elements under a shortlex ordering. Assuming those two properties, let $A$ be the monoid generating set and $M_a$ the multiplier automaton for $a \in A$. Then $\cup_{a \in A} \{ (w_1a, w_2) \mid (w_1,w_2) \in L(M_a) \}$ is a complete regular (and hence recursive) rewriting system for the group, because we can use these rules to replace any word by its unique representative in the wordacceptor language. It is not generally a minimal complete rewriting system, because it may contain redundant rules. For shortlex automatic structures there is a program in the package that computes the unique minimal system. 


What you are really interested in is the word problem for groups. There are many different algorithms for doing this besides representation theory (say, Dehn algorithm is one of the oldest). See http://en.wikipedia.org/wiki/Word_problem_for_groups to get an idea. 

