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", FOCS, 1996, 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, 2013 IEEE 54th Annual Symposium on Foundations of Computer Science 1996, pp. 264, doi:10.1109/SFCS.1996.548485