Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
De Christoph Koutschan
Apparaît dans la collection : Frontiers of reconnaissability / Frontières de la reconnaissabilité
MSO+U is an extension of monadic second-order logic, which adds a quantifier U, called the unbounding quantifier. A formula UX.phi(X) says that phi(X) is true for arbitrarily big finite sets X. The weak fragment (only quantification over finite sets) is decidable over infinite words and trees, while the full logic is undecidable over infinite trees. The decidability results for trees use profinite techniques, while the undecidability results uses descriptive set theory (in fact, the undecidability result is conditional on the set-t heoretic assumption V=L).