Document Open Access Logo

One-Dimensional Logic over Trees

Authors Emanuel Kieronski, Antti Kuusisto

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.64.pdf
  • Filesize: 493 kB
  • 13 pages

Document Identifiers

Author Details

Emanuel Kieronski
Antti Kuusisto

Cite AsGet BibTex

Emanuel Kieronski and Antti Kuusisto. One-Dimensional Logic over Trees. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 64:1-64:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.MFCS.2017.64

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.
Keywords
  • satisfiability
  • expressivity
  • trees
  • fragments of first-order logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski. Extending two-variable logic on trees. In Computer Science Logic, pages 11:1-11:20, 2017. Google Scholar
  2. Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieronski, Rastislav Lenhardt, Filip Mazowiecki, and James Worrell. Complexity of two-variable logic on finite trees. ACM Trans. Comput. Log., 17(4):32:1-32:38, 2016. Google Scholar
  3. Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: http://dx.doi.org/10.1145/322234.322243.
  4. Witold Charatonik, Emanuel Kieronski, and Filip Mazowiecki. Satisfiability of the two-variable fragment of first-order logic over trees. CoRR, abs/1304.7204, 2013. Google Scholar
  5. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and a linear order. In Computer Science Logic, pages 631-647, 2015. Google Scholar
  6. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  7. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Inf. Comput., 179(2):279-295, 2002. URL: http://dx.doi.org/10.1006/inco.2001.2953.
  8. Lauri Hella and Antti Kuusisto. One-dimensional fragment of first-order logic. In Advances in Modal Logic 10, pages 274-293, 2014. Google Scholar
  9. Emanuel Kieronski. On the complexity of the two-variable guarded fragment with transitive guards. Inf. Comput., 204(11):1663-1703, 2006. Google Scholar
  10. Emanuel Kieronski. One-dimensional logic over words. In Computer Science Logic, pages 38:1-38:15, 2016. Google Scholar
  11. Emanuel Kieronski and Antti Kuusisto. Complexity and expressivity of uniform one-dimensional fragment with equality. In Mathematical Foundations of Computer Science, Part I, pages 365-376, 2014. Google Scholar
  12. Emanuel Kieronski and Antti Kuusisto. Uniform one-dimensional fragments with one equivalence relation. In Computer Science Logic, pages 597-615, 2015. Google Scholar
  13. Andreas Krebs, Kamal Lodaya, Paritosh Pandya, and Howard Straubing. Two-variable logic with a between predicate. In Logic in Computer Science, 2016. Google Scholar
  14. Antti Kuusisto. On the uniform one-dimensional fragment. In Proceedings of Description Logic Workshop, 2016. Google Scholar
  15. Maarten Marx. First order paths in ordered trees. In International Conference on Database Theory, pages 114-128, 2005. Google Scholar
  16. Dana Scott. A decision method for validity of sentences in two variables. Journal Symbolic Logic, 27:477, 1962. Google Scholar
  17. Luc Segoufin and Balder ten Cate. Unary negation. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  18. Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, Cambridge, Massachusetts, USA, 1974. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact