Capturing MSO with One Quantifier - Inria - Institut national de recherche en sciences et technologies du numérique
Communication Dans Un Congrès Année : 2015

Capturing MSO with One Quantifier

1 Computer Laboratory [Cambridge] (University of Cambridge Computer Laboratory William Gates Building 15 JJ Thomson Avenue Cambridge CB3 0FD UK - Royaume-Uni)
"> Computer Laboratory [Cambridge]
2 DAHU - Verification in databases (LSV ENS de Cachan 61 avenue du Président Wilson 94235 CACHAN Cedex FRANCE - France)
"> DAHU - Verification in databases
Luc Segoufin

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.
Fichier principal
Vignette du fichier
mso-oneQ.pdf (302.32 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01223378 , version 1 (02-11-2015)

Identifiants

Citer

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⟩
75 Consultations
134 Téléchargements

Altmetric

Partager

More