Equivalence in finite-variable logics is complete for polynomial time

How difficult is it to decide whether two finite structures can be distinguished in a given logic? For first order logic, this question is equivalent to the graph isomorphism problem with its well-known complexity theoretic difficulties. Somewhat surprisingly, the situation is much clearer when considering the fragments L^k of first-order logic whose formulae contain at most k (free or bound) variables (for some k⩾1). We show that for each k⩾2, equivalence in the k-variable logic L^k is complete for polynomial time under quantifier-free reductions (a weak form of NC₀ reductions). Moreover, we show that the same completeness result holds for the powerful extension C^k of L^k with counting quantifiers (for every k⩾2)