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

DOI10.2168/LMCS-11(3:5)2015MaRDI QIDQ3196335zbMATH OpenOpenAlexFDO

Authors Thomas Place, Luc Segoufin

Publication date 29 October 2015

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

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

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)

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.

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}}\)

Cited in

(2)

• scientific article; zbMATH DE number 7104937 (Why is no real title available?)
• scientific article; zbMATH DE number 6000848 (Why is no real title available?)

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)