Proceedings of 37th Conference on Foundations of Computer Science (1996)
Oct. 14, 1996 to Oct. 16, 1996
M. Grohe , Inst. fur Math. Logik, Albert-Ludwigs-Univ., Freiburg, Germany
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/sup k/ of first-order logic whose formulae contain at most k (free or bound) variables (for some k/spl ges/1). We show that for each k/spl ges/2, equivalence in the k-variable logic L/sup k/ is complete for polynomial time under quantifier-free reductions (a weak form of NC/sub 0/ reductions). Moreover, we show that the same completeness result holds for the powerful extension C/sup k/ of L/sup k/ with counting quantifiers (for every k/spl ges/2).
computational complexity; finite-variable logics; equivalence; polynomial time; finite structures; first order logic; graph isomorphism problem; complexity theoretic difficulties; quantifier-free reductions; completeness result; counting quantifiers
M. Grohe, "Equivalence in finite-variable logics is complete for polynomial time," Proceedings of 37th Conference on Foundations of Computer Science(FOCS), Burlington, VT, 1996, pp. 264.