Capturing MSO with One Quantifier
Résumé
We construct a single Lindström quantifier Q such that FO(Q), the extension of first-order logic with Q has the same expressive power as monadic second-order logic on the class of binary trees (with distinct left and right successors) and also on unranked trees with a sibling order. This resolves a conjecture by ten Cate and Segoufin. The quantifier Q is a variation of a quantifier expressing the Boolean satisfiability problem.
Domaines
Informatique et langage [cs.CL]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...