There are many different kinds of groups, and some have better ways of doing them in Wolfram Language. For finite groups there are permutation representations (see the tutorial) For continuous groups with matrix representations, you could go with the matrices. For those that come from a set of functions, you could use functions (and derivatives, etc) But you can also do things completely symbolically, because everything is an expression you can have a symbol mean group product, e.g.,

f[a,b]

You might want it to be able to simplify relations, in which case you can use the Assumptions option in Simplify. This example in the documentation proves Wolfram's Logic axiom implies commutativity (which is the difficult step in showing that the axiom forces f to be Nand. It's not a group but is a good example of Simplify on symbolic expressions)

Simplify[f[a, b] == f[b, a], ForAll[{p, q, r}, f[f[f[p, q], r], f[p, f[f[p, r], p]]] == r]]

Proving that group elements are the same from relations is not trivial (in general undecidable) which is one of the main downsides of this purely symbolic approach (as opposed to a representation as matrices or permutations where most things you want to know would be computable).