License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2017.64
URN: urn:nbn:de:0030-drops-80658
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/8065/
Go to the corresponding LIPIcs Volume Portal

Kieronski, Emanuel ; Kuusisto, Antti

One-Dimensional Logic over Trees

pdf-format:
LIPIcs-MFCS-2017-64.pdf (0.5 MB)

Abstract

A one-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential quantifiers that leave at most one variable free. This fragment contains two-variable logic, and it is known that over words both formalisms have the same complexity and expressive power. Here we investigate the one-dimensional fragment over trees. We consider unranked unordered trees accessible by one or both of the descendant and child relations, as well as ordered trees equipped additionally with sibling relations. We show that over unordered trees the satisfiability problem is ExpSpace-complete when only the descendant relation is available and 2ExpTime-complete with both the descendant and child or with only the child relation. Over ordered trees the problem remains 2ExpTime-complete. Regarding expressivity, we show that over ordered trees and over unordered trees accessible by both the descendant and child the one-dimensional fragment is equivalent to the two-variable fragment with counting quantifiers.

BibTeX - Entry

@InProceedings{kieronski_et_al:LIPIcs:2017:8065,
  author =	{Emanuel Kieronski and Antti Kuusisto},
  title =	{{One-Dimensional Logic over Trees}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{64:1--64:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Kim G. Larsen and Hans L. Bodlaender and Jean-Francois Raskin},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/8065},
  URN =		{urn:nbn:de:0030-drops-80658},
  doi =		{10.4230/LIPIcs.MFCS.2017.64},
  annote =	{Keywords: satisfiability, expressivity, trees, fragments of first-order logic}
}

Keywords: satisfiability, expressivity, trees, fragments of first-order logic
Collection: 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)
Issue Date: 2017
Date of publication: 01.12.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI