Name
Abstract | ||
|---|---|---|
We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of n-element structures that can be distinguished by a k-variable first-order sentence but where every such sentence requires quantifier depth at least nΩ(k / log k). Our trade-offs also apply to first-order counting logic, and by the known connection to the k-dimensional Weisfeiler--Leman algorithm imply near-optimal lower bounds on the number of refinement iterations. A key component in our proof is the hardness condensation technique recently introduced by [Razborov '16] in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the quantifier depth required to distinguish them. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2933575.2934560 | Electronic Colloquium on Computational Complexity (ECCC) |
Keywords | DocType | Volume |
First-order logic, first-order counting logic, bounded variable fragment, quantifier depth, Weisfeiler-Leman, refinement iterations, lower bounds, trade-offs, hardness condensation, XORification | Journal | abs/1608.08704 |
ISSN | ISBN | Citations |
1043-6871 | 978-1-4503-4391-6 | 2 |
PageRank | References | Authors |
0.38 | 29 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christoph Berkholz | 1 | 49 | 7.03 |
| Jakob Nordström | 2 | 177 | 21.76 |