Deciding definability in FO^2(<_v,<_h) on trees

DOI10.2168/LMCS-11(3:5)2015zbMATH Open1448.03025arXiv1505.04934OpenAlexW2207317005MaRDI QIDQ3196335FDOQ3196335

Authors: Thomas Place, Luc Segoufin 

Publication date: 29 October 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: We provide a decidable characterization of regular forest languages definable in FO2(<h,<v). By FO2(<h,<v) we refer to the two variable fragment of first order logic built from the descendant relation and the following sibling relation. In terms of expressive power it corresponds to a fragment of the navigational core of XPath that contains modalities for going up to some ancestor, down to some descendant, left to some preceding sibling, and right to some following sibling. We also show that our techniques can be applied to other two variable first-order logics having exactly the same vertical modalities as FO2(<h,<v) but having different horizontal modalities.

Full work available at URL: https://arxiv.org/abs/1505.04934

Recommendations

• Complexity of two-variable logic on finite trees
• Complexity of two-variable logic on finite trees
• STACS 2005
• Regular tree languages definable in FO and in FO\(_{\mathrm{mod}}\)

zbMATH Keywords

characterizationtree automatatree languagestwo-variables first-order logic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25)

Cited In (2)

• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: Deciding definability in \(\mathrm{FO}^2(<_{\mathbf{v}},<_{\mathbf{h}})\) on trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196335)