Order-Invariance of Two-Variable Logic is coNExpTime-complete
Bartosz Bednarczyk
TL;DR
This paper proves that determining whether a two-variable first-order logic formula is order-invariant is a computationally complex problem, specifically coNExpTime-complete, improving previous bounds.
Contribution
It establishes the exact complexity of order-invariance decision for two-variable logic, simplifying earlier bounds and providing a definitive classification.
Findings
Deciding order-invariance is coNExpTime-complete.
The complexity bound improves previous results.
The proof simplifies the understanding of the problem's difficulty.
Abstract
We establish coNExpTime-completeness of the problem of deciding order-invariance of a given two variable first-order formula, improving and significantly simplifying coTwoNExpTime bound by Zeume and Harwath.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Advanced Algebra and Logic · semigroups and automata theory