Document Open Access Logo

Extending Two-Variable Logic on Trees

Authors Bartosz Bednarczyk, Witold Charatonik, Emanuel Kieronski

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2017.11.pdf
  • Filesize: 0.6 MB
  • 20 pages

Document Identifiers

Subject Classification

Keywords
  • two-variable logic
  • trees
  • satisfiability
  • expressivity
  • counting quantifiers

Metrics

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

Abstract

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

Cite As Get BibTex

Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski. Extending Two-Variable Logic on Trees. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.11

Author Details

Bartosz Bednarczyk
Witold Charatonik
Emanuel Kieronski

References

  1. Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski. Extending two-variable logic on trees. CoRR, abs/1611.02112, 2016. URL: http://arxiv.org/abs/1611.02112.
  2. Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieroński, Rastislav Lenhardt, Filip Mazowiecki, and James Worrell. Complexity of two-variable logic on finite trees. ACM Transactions on Computational Logic, 17(4):32:1-32:38, 2017. Extended abstract in ICALP 2013. Google Scholar
  3. M. Bojanczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words. ACM Transactions on Computational Logic, 12(4):27, 2011. Google Scholar
  4. M. Bojanczyk, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data trees and XML reasoning. Journal of the ACM, 56(3), 2009. Google Scholar
  5. 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
  6. Witold Charatonik, Emanuel Kieroński, and Filip Mazowiecki. Decidability of weak logics with deterministic transitive closure. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS'14, Vienna, Austria, July 14-18, 2014, page 29, 2014. URL: http://dx.doi.org/10.1145/2603088.2603134.
  7. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and a linear order. Logical Methods in Computer Science, 12(2), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(2:8)2016.
  8. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and trees. ACM Transactions on Computational Logic, 17(4):31:1-31:27, 2017. Extended abstract in LICS 2013. Google Scholar
  9. Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. Vector addition tree automata. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 64-73. IEEE Computer Society, 2004. URL: http://dx.doi.org/10.1109/LICS.2004.1319601.
  10. 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.
  11. Diego Figueira. Satisfiability for two-variable logic with two successor relations on finite linear orders. Computing Research Repository, abs/1204.2495, 2012. Google Scholar
  12. E. Grädel, P. Kolaitis, and M. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  13. E. Grädel, M. Otto, and E. Rosen. Two-variable logic with counting is decidable. In LICS 1997, Proceedings, pages 306-317, 1997. Google Scholar
  14. Emanuel Kieroński. Results on the guarded fragment with equivalence or transitive relations. In C.-H. Luke Ong, editor, CSL, volume 3634 of Lecture Notes in Computer Science, pages 309-324. Springer, 2005. URL: http://dx.doi.org/10.1007/11538363_22.
  15. Emanuel Kieroński. Decidability issues for two-variable logics with several linear orders. In Marc Bezem, editor, CSL, volume 12 of LIPIcs, pages 337-351. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2011.337.
  16. Emanuel Kieroński, Jakub Michaliszyn, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. In LICS, pages 431-440. IEEE Computer Society, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.53.
  17. Emanuel Kieroński and Martin Otto. Small substructures and decidability issues for first-order logic with two variables. In LICS, pages 448-457. IEEE Computer Society, 2005. URL: http://dx.doi.org/10.1109/LICS.2005.49.
  18. Emanuel Kieroński and Lidia Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In LICS, pages 123-132. IEEE Computer Society, 2009. URL: http://dx.doi.org/10.1109/LICS.2009.39.
  19. Amaldev Manuel. Two variables and two successors. In Petr Hlinený and Antonín Kucera, editors, MFCS, volume 6281 of Lecture Notes in Computer Science, pages 513-524. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15155-2_45.
  20. Maarten Marx and Maarten de Rijke. Semantic characterization of navigational XPath. In First Twente Data Management Workshop (TDM 2004) on XML Databases and Information Retrieval, pages 73-79, 2004. Google Scholar
  21. Martin Otto. Two variable first-order logic over ordered domains. J. Symb. Log., 66(2):685-702, 2001. Google Scholar
  22. Leszek Pacholski, Wieslaw Szwast, and Lidia Tendera. Complexity of two-variable logic with counting. In LICS, pages 318-327, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614958.
  23. I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information, 14(3):369-395, 2005. Google Scholar
  24. I. Pratt-Hartmann. Logics with counting and equivalence. In CSL-LICS 2014, Proceedings, page 76, 2014. Google Scholar
  25. Thomas Schwentick and Thomas Zeume. Two-variable logic with two order relations - (extended abstract). In Anuj Dawar and Helmut Veith, editors, CSL, volume 6247 of Lecture Notes in Computer Science, pages 499-513. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15205-4_38.
  26. Dana Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27:477, 1962. Google Scholar
  27. Thomas Zeume and Frederik Harwath. Order-invariance of two-variable logic is decidable. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16, pages 807-816, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2933575.2933594.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact