Document Open Access Logo

On the Limits of Decision: the Adjacent Fragment of First-Order Logic

Authors Bartosz Bednarczyk , Daumantas Kojelis , Ian Pratt-Hartmann

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.111.pdf
  • Filesize: 0.89 MB
  • 21 pages

Document Identifiers

Author Details

Bartosz Bednarczyk
  • Computational Logic Group, Technische Universität Dresden, Germany
  • Institute of Computer Science, University of Wrocław, Poland
Daumantas Kojelis
  • Department of Computer Science, University of Manchester, UK
Ian Pratt-Hartmann
  • Department of Computer Science, University of Manchester, UK
  • Institute of Computer Science, University of Opole, Poland

Funding

  • Bednarczyk, Bartosz: supported by the ERC Consolidator Grant No. 771779 (https://iccl.inf.tu-dresden.de/web/DeciGUT/en).
  • Pratt-Hartmann, Ian: supported by the NCN grant 2018/31/B/ST6/03662.

Acknowledgements

B. Bednarczyk thanks R. Jaakkola for many inspiring discussions.

Cite As Get BibTex

Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann. On the Limits of Decision: the Adjacent Fragment of First-Order Logic. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 111:1-111:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ICALP.2023.111

Abstract

We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • decidability
  • satisfiability
  • variable-ordered logics
  • complexity

Metrics

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

Related Versions

References

  1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998. URL: https://doi.org/10.1023/a:1004275029985.
  2. Bartosz Bednarczyk. Exploiting forwardness: Satisfiability and query-entailment in forward guarded fragment. In Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak, editors, Logics in Artificial Intelligence - 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, volume 12678 of Lecture Notes in Computer Science, pages 179-193. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-75775-5_13.
  3. Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieroński. Extending two-variable logic on trees. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 11:1-11:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.11.
  4. Bartosz Bednarczyk and Reijo Jaakkola. Towards a model theory of ordered logics: Expressivity and interpolation. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 of LIPIcs, pages 15:1-15:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.15.
  5. Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann. On the limits of decision: the adjacent fragment of first-order logic. ArXiV, abs/2305.03133, 2023. URL: https://arxiv.org/abs/2305.03133.
  6. Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two variable logic with ultimately periodic counting. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 112:1-112:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.112.
  7. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Transactions on Computational Logic, 12(4), July 2011. URL: https://doi.org/10.1145/1970398.1970403.
  8. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  9. Witold Charatonik, Emanuel Kieroński, and Filip Mazowiecki. Decidability of weak logics with deterministic transitive closure. In Thomas A. Henzinger and Dale Miller, editors, 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, pages 29:1-29:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603134.
  10. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and trees. ACM Transactions on Computational Logic, 17(4), November 2016. URL: https://doi.org/10.1145/2983622.
  11. Erich Grädel. On the restraining power of guards. The Journal of Symbolic Logic, 64(4):1719-1742, 1999. URL: http://www.jstor.org/stable/2586808.
  12. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic, 3(1):53-69, 1997. URL: http://www.jstor.org/stable/421196.
  13. Leon Henkin. Logical Systems Containing Only a Finite Number of Symbols. Séminaire de mathématiques supérieures. Presses de l'Université de Montréal, 1967. URL: https://books.google.pl/books?id=0jPQAAAAMAAJ.
  14. Andreas Herzig. A new decidable fragment of first order logic. In Abstracts of the 3rd Logical Biennial Summer School and Conference in honour of S. C. Kleene, Varna, Bulgaria, June 1990. Google Scholar
  15. David Hilbert and Wilhelm Ackermann. Grundzüge der theoretischen Logik. Springer, Berlin, 1928. Google Scholar
  16. David Hilbert and Wilhelm Ackermann. Principles of Mathematical Logic. Chelsea, New York, 1950. Google Scholar
  17. Ullrich Hustadt, Renate A Schmidt, and Lilia Georgieva. A survey of decidable first-order fragments and description logics. Journal of Relational Methods in Computer Science, 1(3):251-276, 2004. Google Scholar
  18. Reijo Jaakkola. Ordered fragments of first-order logic. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia, volume 202 of LIPIcs, pages 62:1-62:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.62.
  19. Emanuel Kieroński. One-dimensional guarded fragments. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 16:1-16:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.16.
  20. Emanuel Kieroński and Jakub Michaliszyn. Two-variable universal logic with transitive closure. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 396-410. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.396.
  21. Emanuel Kieroński, Jakub Michaliszyn, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. SIAM Journal on Computing, 43(3):1012-1063, 2014. URL: https://doi.org/10.1137/120900095.
  22. Emanuel Kieroński and Martin Otto. Small substructures and decidability issues for first-order logic with two variables. Journal of Symbolic Logic, 77(3):729-765, 2012. URL: https://doi.org/10.2178/jsl/1344862160.
  23. Emanuel Kieroński, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable logics with counting and semantic constraints. ACM SIGLOG News, 5(3):22-43, 2018. URL: https://doi.org/10.1145/3242953.3242958.
  24. Emanuel Kieroński and Lidia Tendera. On finite satisfiability of two-variable first-order logic with equivalence relations. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 123-132. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.39.
  25. Amaldev Manuel. Two variables and two successors. In Petr Hlinený and Antonín Kucera, editors, Mathematical Foundations of Computer Science 2010, 35th International Symposium, MFCS 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6281 of Lecture Notes in Computer Science, pages 513-524. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15155-2_45.
  26. Ian Pratt-Hartmann. The two-variable fragment with counting revisited. In Anuj Dawar and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings, volume 6188 of Lecture Notes in Computer Science, pages 42-54. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13824-9_4.
  27. Ian Pratt-Hartmann. Finite satisfiability for two-variable, first-order logic with one transitive relation is decidable. Mathematical Logic Quarterly, 64(3):218-248, 2018. URL: https://doi.org/10.1002/malq.201700055.
  28. Ian Pratt-Hartmann. Fluted logic with counting. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 141:1-141:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.141.
  29. Ian Pratt-Hartmann. Walking on words. ArXiV, abs/2208.08913, 2022. URL: https://doi.org/10.48550/arXiv.2208.08913.
  30. Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. The fluted fragment revisited. Journal of Symbolic Logic, 84(3):1020-1048, 2019. Google Scholar
  31. Ian Pratt-Hartmann and Lidia Tendera. The fluted fragment with transitive relations. Annals of Pure and Applied Logic, 173(1):103042, 2022. URL: https://doi.org/10.1016/j.apal.2021.103042.
  32. William C. Purdy. Fluted formulas and the limits of decidability. The Journal of Symbolic Logic, 61(2):608-620, 1996. URL: http://www.jstor.org/stable/2275678.
  33. Willard Van Orman Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62. University of Vienna, 1969. Google Scholar
  34. Willard Van Orman Quine. Algebraic logic and predicate functors. In The Ways of Paradox, pages 283-307. Harvard University Press, Cambridge, MA, revised and enlarged edition, 1976. Google Scholar
  35. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computational Logic, 8(1), February 2016. URL: https://doi.org/10.1145/2858784.
  36. Thomas Schwentick and Thomas Zeume. Two-Variable Logic with Two Order Relations. Logical Methods in Computer Science, Volume 8, Issue 1, March 2012. URL: https://doi.org/10.2168/LMCS-8(1:15)2012.
  37. Thomas Zeume and Frederik Harwath. Order-invariance of two-variable logic is decidable. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 807-816. ACM, 2016. URL: https://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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact