Tree Canonization and Transitive Closure

We prove that tree isomorphism is not expressible in the language (FO + TC + COUNT). This is surprising since in the presence of ordering the language captures NL, whereas tree isomorphism and canonization are in L ( Lin92]). Our proof uses an Ehrenfeucht-Fra sse game for transitive closure logic with counting Gra91, IL90]. As a corresponding upper bound, we show that tree canonization is expressible in (FO+COUNT) logn]. The best previous upper bound had been (FO+COUNT) nO(1) ] ( DM90]). The lower bound remains true for bounded-degree trees, and we show that for bounded-degree trees counting is not needed in the upper bound. These results are the rst separations of the unordered versions of the logical languages for NL, AC1 , and ThC1 . Our results were motivated by our conjecture in EI95] that (FO+TC+COUNT+ 1LO) = NL, i.e., that a one-way local ordering su ced to capture NL. We disprove this conjecture, but we prove that a two-way local ordering does su ce, i.e., (FO + TC + COUNT+ 2L...

• Type: Conference
• Year: 1995
• Where: LICS
• Authors: Kousha Etessami, Neil Immerman
• Keywords: Automated Reasoning, Corresponding Upper Bound, LICS 1995, Tree Isomorphism, Upper Bound