Tree Automata Make Ordinal Theory Easy
Thierry Cachat · arXiv (Cornell University) · 2006
We give a new simple proof of the decidability of the First Order Theory of $(w^{w^i},+)$ and the Monadic Second Order Theory of $(w^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.