Document

One-Dimensional Logic over Trees

File

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

Cite As

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

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.
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.
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.
5. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and a linear order. In Computer Science Logic, pages 631-647, 2015.
6. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995.
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.
9. Emanuel Kieronski. On the complexity of the two-variable guarded fragment with transitive guards. Inf. Comput., 204(11):1663-1703, 2006.
10. Emanuel Kieronski. One-dimensional logic over words. In Computer Science Logic, pages 38:1-38:15, 2016.
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.
12. Emanuel Kieronski and Antti Kuusisto. Uniform one-dimensional fragments with one equivalence relation. In Computer Science Logic, pages 597-615, 2015.
13. Andreas Krebs, Kamal Lodaya, Paritosh Pandya, and Howard Straubing. Two-variable logic with a between predicate. In Logic in Computer Science, 2016.
14. Antti Kuusisto. On the uniform one-dimensional fragment. In Proceedings of Description Logic Workshop, 2016.
15. Maarten Marx. First order paths in ordered trees. In International Conference on Database Theory, pages 114-128, 2005.
16. Dana Scott. A decision method for validity of sentences in two variables. Journal Symbolic Logic, 27:477, 1962.
17. Luc Segoufin and Balder ten Cate. Unary negation. Logical Methods in Computer Science, 9(3), 2013.
18. Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, Cambridge, Massachusetts, USA, 1974.
X

Feedback for Dagstuhl Publishing