In the general case, to determine whether some relations imply another given relation is an undecidable problem. If it were decidable, then we could decide whether a given finite presentation was a presenting the trivial group (a known undecidable problem), by testing whether the generators are all redundant.

In the general case, to determine whether some relations imply another given relation is an undecidable problem. If it were decidable, then we could decide whether a given finite presentation was presenting the trivial group or not (a known undecidable problem), by testing whether the generators are all redundant as relations.