Mateus de Oliveira Oliveira: The Parameterized Complexity of Equational Logic

We introduce a variant of equational logic in which sentences are pairs of the form (s=t, ω) where ω is an arbitrary ordering of the sub-terms appearing in s=t. To each ordered equation (s=t, ω) one may naturally associate a notion of width, and to each derivation of an ordered equation (s=t, ω) from a set of axioms E, one may naturally define a notion of depth. The width of such a derivation is defined as the width of the thickest ordered equation appearing in it. Our main result states that for any fixed set of axioms E and constants c and d one may determine whether a given ordered equation (s=t, ω) can be inferred from E in depth d and width c in time f (|E|, d, c)*|s = t|^O(c) . Additionally we will define the notion of b-bounded substitution. We say that a proof is b- bounded if every substitution rule used on it is b-bounded. We will show that one may determine whether (s=t, ω) follows from E via a b-bounded proof of depth d and width c in time f (|E|, d, c, b)|s = t|.