Capturing MSO with One Quantifier

Anuj Dawar 1 Luc Segoufin 2
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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 metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01223378
Contributor : Luc Segoufin <>
Submitted on : Monday, November 2, 2015 - 3:30:18 PM
Last modification on : Thursday, February 7, 2019 - 5:29:22 PM
Long-term archiving on : Wednesday, February 3, 2016 - 10:52:56 AM

File

mso-oneQ.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

167

Files downloads

156