The First-Order Theory of Ground Tree Rewrite Graphs
Logic in Computer Science
2015-07-01 v4 Computational Complexity
Abstract
We prove that the complexity of the uniform first-order theory of ground tree rewrite graphs is in ATIME(2^{2^{poly(n)}},O(n)). Providing a matching lower bound, we show that there is some fixed ground tree rewrite graph whose first-order theory is hard for ATIME(2^{2^{poly(n)}},poly(n)) with respect to logspace reductions. Finally, we prove that there exists a fixed ground tree rewrite graph together with a single unary predicate in form of a regular tree language such that the resulting structure has a non-elementary first-order theory.
Keywords
Cite
@article{arxiv.1107.0919,
title = {The First-Order Theory of Ground Tree Rewrite Graphs},
author = {Stefan Göller and Markus Lohrey},
journal= {arXiv preprint arXiv:1107.0919},
year = {2015}
}
Comments
accepted for Logical Methods in Computer Science