In this work we study the validity problem in equational logic under the perspective of parameterized complexity theory. First we introduce a variant of equational logic in which sentences are pairs of the form $(t_1=t_2,omega)$ where $omega$ is an arbitrary ordering of the positions corresponding to subterms of $t_1$ and $t_2$. We call such pairs {em ordered equations}. To each ordered equation one may naturally associate a notion of width and to each proof of validity of an ordered equation one may naturally associate a notion of depth. We define the width of such a proof to be the maximum width of an ordered equation occurring in it. Finally, we introduce a parameter $b$ which restricts the way in which variables are substituted for terms. We say that a proof is $b$-bounded if all substitutions used in it satisfy such restriction.
In a surprising result, we show that one may determine whether an ordered equation $(t_1=t_2,omega)$ has a $b$-bounded proof of width $c$ and depth $d$... more