Abstract / Description of output
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 (Lindell, 1992). Our proof uses an Ehrenfeucht-Fraisse game for transitive closure logic with counting. As a corresponding upper bound, we show that tree canonization is expressible in (FO+COUNT)[log n]. The best previous upper bound had been (FO+COUNT)[n 0(1)] (Dublish and Maheshwari, 1990). 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 first separations of the unordered versions of the logical languages for NL, AC1, and ThC1. Our results were motivated by a conjecture in (Etessami and Immerman, 1995) that (FO+TC+COUNT+1LO)=NL, i.e., that a one-way local ordering sufficed to capture NL. We disprove this conjecture, but we prove that a two-way local ordering does suffice, i.e., (FO+TC+COUNT+2LO)=NL
Original language | English |
---|---|
Title of host publication | Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995 |
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
Pages | 331-341 |
Number of pages | 11 |
ISBN (Print) | 0-8186-7050-9 |
DOIs | |
Publication status | Published - 1995 |