This should be a comment but is too long. The decidability of the question whether a finite set R of relations implies some other relation r=1 in all linear groups is the same as asking if R implies r=1 in all finite groups because of Malcev's theorem on residual finiteness of linear groups. A beautiful theorem of Slobodoskoii says this latter problem is undecidable. 

A consequence is that the first order theory for finite dimensional modules over an algebra of wild representation type is undecidable. (Most books on finite dimensional algebras mistakenly assert it follows from undecidability of the word problem for groups, but one must then allow infinite dimensional modules.)