Skip to Main content Skip to Navigation
New interface
Conference papers

Capturing MSO with One Quantifier

Anuj Dawar 1 Luc Segoufin 2 
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Luc Segoufin Connect in order to contact the contributor
Submitted on : Monday, November 2, 2015 - 3:30:18 PM
Last modification on : Wednesday, February 2, 2022 - 3:53:50 PM
Long-term archiving on: : Wednesday, February 3, 2016 - 10:52:56 AM


Files produced by the author(s)



Anuj Dawar, Luc Segoufin. Capturing MSO with One Quantifier. Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday., 2015, Berlin, Germany. ⟨10.1007/978-3-319-23534-9_8⟩. ⟨hal-01223378⟩



Record views


Files downloads