Search

• < Previous
• 1
• Next >

Recursion Schemes, the MSO Logic, and the U quantifier

We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known to be decidable for sentences of the MSO logic. We prove decidability for an extension of MSO in which we additionally&nbsp;[&hellip;]