Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler - Leman Refinement Steps
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler - Leman Refinement Steps. / Berkholz, Christoph; Nordström, Jakob.
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016. Institute of Electrical and Electronics Engineers Inc., 2016. s. 267-276 (Proceedings - Symposium on Logic in Computer Science, Bind 05-08-July-2016).Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler - Leman Refinement Steps
AU - Berkholz, Christoph
AU - Nordström, Jakob
PY - 2016/7/5
Y1 - 2016/7/5
N2 - 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.
AB - 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.
KW - bounded variable fragment
KW - first-order counting logic
KW - First-order logic
KW - hardness condensation
KW - lower bounds
KW - quantifier depth
KW - refinement iterations
KW - trade-offs
KW - Weisfeiler - Leman
KW - XORification
UR - http://www.scopus.com/inward/record.url?scp=84994626925&partnerID=8YFLogxK
U2 - 10.1145/2933575.2934560
DO - 10.1145/2933575.2934560
M3 - Article in proceedings
AN - SCOPUS:84994626925
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 267
EP - 276
BT - Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
Y2 - 5 July 2016 through 8 July 2016
ER -
ID: 251868527