Document Open Access Logo

Uniform One-Dimensional Fragments with One Equivalence Relation

Authors Emanuel Kierónski, Antti Kuusisto

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.597.pdf
  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Emanuel Kierónski
Antti Kuusisto

Cite AsGet BibTex

Emanuel Kierónski and Antti Kuusisto. Uniform One-Dimensional Fragments with One Equivalence Relation. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 597-615, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CSL.2015.597

Abstract

The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.
Keywords
  • two-variable logic
  • uniform one-dimensional fragments
  • complexity
  • expressivity
  • equivalence relations

Metrics

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

References

  1. H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27:217-274, 1998. Google Scholar
  2. V. Bárány, B. ten Cate, and L. Segoufin. Guarded negation. In ICALP 2011, Proceedings Part II, pages 356-367, 2011. Google Scholar
  3. S. Benaim, M. Benedikt, W. Charatonik, E. nski, R. Lenhardt, F. Mazowiecki, and J. Worrell. Complexity of two-variable logic on finite trees. In ICALP 2013, Proceedings Part II, pages 74-88, 2013. Google Scholar
  4. 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
  5. 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
  6. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer, 1885. Google Scholar
  7. 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
  8. 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
  9. L. Hella and A. Kuusisto. One-dimensional fragment of first-order logic. In AIML 2014, Proceedings, pages 274-293, 2014. Google Scholar
  10. E. Kieronski and A. Kuusisto. Complexity and expressivity of uniform one-dimensional fragment with equality. In MFCS 2014, Proceedings Part I, pages 365-376, 2014. Google Scholar
  11. E. Kieronski, J. Michaliszyn, I. Pratt-Hartmann, and L. Tendera. Two-variable first-order logic with equivalence closure. SIAM Journal on Computing, 43(3):1012-1063, 2014. Google Scholar
  12. E. Kieronski and M. Otto. Small substructures and decidability issues for first-order logic with two variables. Journal of Symbolic Logic, 77:729-765, 2012. Google Scholar
  13. E. Kieronski and L. Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In LICS 2009, Proceedings, pages 123-132, 2009. Google Scholar
  14. B. ten Cate L. Segoufin. Unary negation. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  15. L. Libkin. Elements of Finite Model Theory. Springer, 2004. Google Scholar
  16. A. Montanari and P. Sala. Adding an equivalence relation to the interval logic AB̄B: complexity and expressiveness. In LICS 2013, Proceedings, pages 193-202, 2013. Google Scholar
  17. M. Mortimer. On languages with two variables. Zeitschr. f. math. Logik u. Grundlagen d. Math., 21:135–140, 1975. Google Scholar
  18. L. Pacholski, W. Szwast, and L. Tendera. Complexity of two-variable logic with counting. In LICS 1997, Proceedings, pages 318-327, 1997. Google Scholar
  19. C.H. Papadimitriou. Computational Complexity. Addison Wesley Longman, 1994. Google Scholar
  20. 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
  21. I. Pratt-Hartmann. Logics with counting and equivalence. In CSL-LICS 2014, Proceedings, page 76, 2014. Google Scholar
  22. D. Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27:477, 1962. Google Scholar
  23. W. Szwast and L. Tendera. FO² with one transitive relation is decidable. In STACS 2013, Proceedings, pages 317-328, 2013. 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