Equivalence in finite-variable logics is complete for polynomial time (Q1977423)

In this paper the author investigates the complexity of equivalence checking in finite variable logics. The main result says that for each \(k\geq 2\) there is an \(\text{AC}_0\)-reduction from MONOTONE CIRCUIT VALUE to \(E(k)\) and \(T(k)\). From this theorem follows that for a logic \({\mathtt L}\in \{{\mathtt L}^k,{\mathtt C}^k \mid k\geq 2\}\) the problems \({\mathtt L}\)-EQUIVALENCE (if two directed graphs are equivalent in \({\mathtt L}\)) and \({\mathtt L}\)-TYPE (if two vertices of a directed graph \(G\) have the same \({\mathtt L}\)-type) are complete for polynomial time under uniform \(\text{AC}_0\)-reductions. Several other important corollaries are obtained.