TL;DR
This paper introduces a tree automata-based method to simplify and improve the decidability and complexity of theories related to ordinals and their orderings, using a novel representation of sets of ordinals as infinite trees.
Contribution
It provides a new, simpler proof of decidability for certain ordinal theories and enhances complexity bounds through a novel automata-based approach.
Findings
Decidability of the First Order Theory of (omega^omega^i,+)
Decidability of the Monadic Second Order Theory of (omega^i,<)
Improved complexity bounds for these theories
Abstract
We give a new simple proof of the decidability of the First Order Theory of (omega^omega^i,+) and the Monadic Second Order Theory of (omega^i,<), improving the complexity in both cases. Our algorithm is based on tree automata and a new representation of (sets of) ordinals by (infinite) trees.
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.