An optimal construction of Hanf sentences
Benedikt Bollig, Dietrich Kuske
TL;DR
This paper presents an elementary method for constructing equivalent Hanf normal form formulas, establishing both an upper and lower bound of triply exponential complexity.
Contribution
It provides the first elementary construction of Hanf normal form formulas with matching bounds, advancing understanding of their complexity.
Findings
Established a triply exponential upper bound.
Proved a matching triply exponential lower bound.
Introduced an elementary construction method.
Abstract
We give the first elementary construction of equivalent formulas in Hanf normal form. The triply exponential upper bound is complemented by a matching lower bound.
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.