Document Open Access Logo

One-Dimensional Logic over Words

Author Emanuel Kieronski

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.38.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

Emanuel Kieronski

Cite AsGet BibTex

Emanuel Kieronski. One-Dimensional Logic over Words. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 38:1-38:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.38

Abstract

One-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential quantifiers that leave at most one variable free. We investigate one-dimensional fragment over words and over omega-words. We show that it is expressively equivalent to the two-variable fragment of first-order logic. We also show that its satisfiability problem is NExpTime-complete. Further, we show undecidability of some extensions, whose two-variable counterparts remain decidable.
Keywords
  • satisfiability
  • expressivity
  • words
  • fragments of first-order logic

Metrics

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

References

  1. Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieroński, Rastislav Lenhardt, Filip Mazowiecki, and James Worrell. Complexity of two-variable logic on finite trees. In ICALP (2), pages 74-88, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39212-2_10.
  2. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27, 2011. Google Scholar
  3. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and trees. In LICS, pages 73-82, 2013. Google Scholar
  4. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and a linear order. In Computer Science Logic, volume 41 of LIPIcs, pages 631-647, 2015. Google Scholar
  5. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  6. 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.
  7. Erich Grädel, Phokion Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  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 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
  10. Emanuel Kieronski and Antti Kuusisto. Uniform one-dimensional fragments with one equivalence relation. In Computer Science Logic, volume 41 of LIPIcs, pages 597-615, 2015. Google Scholar
  11. Emanuel Kieroński and Martin Otto. Small substructures and decidability issues for first-order logic with two variables. Journal of Symbolic Logic, 77:729-765, 2012. Google Scholar
  12. Andreas Krebs, Kamal Lodaya, Paritosh Pandya, and Howard Straubing. Two-variable logic with a between predicate. In LICS, 2016. Google Scholar
  13. Antti Kuusisto. On the uniform one-dimensional fragment. In Proceedings of International Workshop on Description Logic, 2016. Google Scholar
  14. Angelo Montanari, Marco Pazzaglia, and Pietro Sala. Metric propositional neighborhood logic with an equivalence relation. In TIME, pages 49-58, 2014. Google Scholar
  15. Martin Otto. Two-variable first-order logic over ordered domains. Journal of Symbolic Logic, 66:685-702, 2001. Google Scholar
  16. Thomas Schwentick and Thomas Zeume. Two-variable logic with two order relations. Logical Methods in Computer Science, 8(1), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:15)2012.
  17. Dana Scott. A decision method for validity of sentences in two variables. Journal Symbolic Logic, 27:477, 1962. Google Scholar
  18. Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, Cambridge, Massasuchets, USA, 1974. Google Scholar
  19. Wieslaw Szwast and Lidia Tendera. FO² with one transitive relation is decidable. In STACS, 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