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.
Type de document :
Communication dans un congrès
Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday., 2015, Berlin, Germany. 9300, 2015, LNCS. 〈10.1007/978-3-319-23534-9_8〉
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01223378
Contributeur : Luc Segoufin <>
Soumis le : lundi 2 novembre 2015 - 15:30:18
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : mercredi 3 février 2016 - 10:52:56

Fichier

mso-oneQ.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. 9300, 2015, LNCS. 〈10.1007/978-3-319-23534-9_8〉. 〈hal-01223378〉

Partager

Métriques

Consultations de la notice

120

Téléchargements de fichiers

60