Let $\Sigma = \{a, b, c, ..., x, y, w\}$ be a set of formal variables, $\Sigma^{-1} = \{a^{-1}, b^{-1}, ..., w^{-1}\}$ be the inverses of those variables, and $B = \{ e_1, e_2, ..., e_n \}$ be a set of equations involving products of those variables and their inverses in the left hand side and one in the right side.
So, each $e_i$ is of the form $\Pi_{i=1}^m \bar{x}_i = 1$ with $\bar{x}_i \in \Sigma \cup \Sigma^{-1}$.
Also, assume that those variables do not commute.
For instance, we could have $e_1$ as $axk^{-1} = 1$, $e_2$ as $k^{-1}xak = 1$, $e_3$ as $b^2xyx = 1$, etc.
Is there a general algorithm to decide if a new equation $e_{n+1}$ with the same format is a consequence of those in $B$?
PS: In fact, this is the problem of deciding if a given relation $e_{n+1}$ of a finitely presented group $\langle \Sigma | B\cup \{e_{n+1}\} \rangle$ can be derived from the relations in $B$...