Recursion Schemes and the WMSO+U Logic
Paweł Parys · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2018
We study the weak MSO logic extended by the unbounding quantifier (WMSO+U), expressing the fact that there exist arbitrarily large finite sets satisfying a given property. We prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+U.