Document Open Access Logo

The Guarded Fragment with Nested Equivalences

Author Oskar Fiuk

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.44.pdf
  • Filesize: 0.9 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • guarded fragment
  • finite model property
  • nested equivalence relations

Metrics

Abstract

The Guarded Fragment (GF) is a well-established decidable fragment of first-order logic. We study an extension of GF with nested equivalence relations, namely a family of distinguished binary predicates E₁, E₂, … interpreted as equivalence relations such that E_{k+1} is coarser than E_k for every k. We show that the equality-free GF with nested equivalence relations enjoys the finite model property and has a decidable satisfiability problem. Moreover, we establish tight complexity bounds for satisfiability: Tower-completeness in general, and (K{+}2)-ExpTime-completeness when the number of distinguished predicates is fixed to K. Finally, we show that satisfiability becomes undecidable if either the nesting condition is dropped (already with two equivalence relations) or equality is admitted (already with a single equivalence relation).

Cite As Get BibTex

Oskar Fiuk. The Guarded Fragment with Nested Equivalences. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 44:1-44:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.44

Author Details

Oskar Fiuk
  • Institute of Computer Science, University of Wrocław, Poland

Funding

Polish National Science Center, grant No. 2021/41/B/ST6/00996.

Acknowledgements

The author thanks Emanuel Kieroński for helpful discussions, and the reviewers of LICS 2026 for their valuable suggestions.

References

  1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. J. Philos. Log., 27(3):217-274, 1998. URL: https://doi.org/10.1023/A:1004275029985.
  2. Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. URL: http://www.cambridge.org/de/academic/subjects/computer-science/knowledge-management-databases-and-data-mining/introduction-description-logic?format=PB#17zVGeWD2TZUeu6s.97.
  3. Vince Bárány, Georg Gottlob, and Martin Otto. Querying the guarded fragment. Log. Methods Comput. Sci., 10(2), 2014. URL: https://doi.org/10.2168/LMCS-10(2:3)2014.
  4. 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, 2016. URL: https://doi.org/10.1145/2996796.
  5. Henrik Björklund and Mikolaj Bojanczyk. Shuffle expressions and words with nested data. In Ludek Kucera and Antonín Kucera, editors, Mathematical Foundations of Computer Science 2007, 32nd International Symposium, MFCS 2007, Ceský Krumlov, Czech Republic, August 26-31, 2007, Proceedings, volume 4708 of Lecture Notes in Computer Science, pages 750-761. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74456-6_66.
  6. Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. J. ACM, 56(3):13:1-13:48, 2009. URL: https://doi.org/10.1145/1516512.1516515.
  7. Egon Börger, Erich Grädel, and Yuri Gurevich. The classical decision problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  8. Alexander Borgida. On the relative expressiveness of description logics and predicate logics. Artif. Intell., 82(1-2):353-367, 1996. URL: https://doi.org/10.1016/0004-3702(96)00004-5.
  9. Pierre Bourhis, Michael Morak, and Andreas Pieris. Making cross products and guarded ontology languages compatible. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 880-886. ijcai.org, 2017. URL: https://doi.org/10.24963/ijcai.2017/122.
  10. Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  11. Witold Charatonik and Piotr Witkowski. Two-variable logic with counting and trees. ACM Trans. Comput. Log., 17(4):31, 2016. URL: https://doi.org/10.1145/2983622.
  12. Daniel Danielski and Emanuel Kieronski. Finite satisfiability of unary negation fragment with transitivity. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, Aachen, Germany, August 26-30, 2019, volume 138 of LIPIcs, pages 17:1-17:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.17.
  13. Oskar Fiuk, Emanuel Kieroński, and Vincent Michielini. Two-Variable Logic for Hierarchically Partitioned and Ordered Data. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning, pages 316-325, October 2025. URL: https://doi.org/10.24963/kr.2025/31.
  14. Warren D. Goldfarb. The unsolvability of the godel class with identity. J. Symb. Log., 49(4):1237-1252, 1984. URL: https://doi.org/10.2307/2274274.
  15. Erich Grädel. On the restraining power of guards. J. Symb. Log., 64(4):1719-1742, 1999. URL: https://doi.org/10.2307/2586808.
  16. Ian Horrocks and Ulrike Sattler. A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput., 9(3):385-410, 1999. URL: https://doi.org/10.1093/logcom/9.3.385.
  17. Emanuel Kieronski. Results on the guarded fragment with equivalence or transitive relations. In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 309-324. Springer, 2005. URL: https://doi.org/10.1007/11538363_22.
  18. Emanuel Kieronski and Adam Malinowski. The triguarded fragment with transitivity. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 334-353. EasyChair, 2020. URL: https://doi.org/10.29007/z359.
  19. Emanuel Kieronski, Jakub Michaliszyn, Ian Pratt-Hartmann, and Lidia Tendera. Two-variable first-order logic with equivalence closure. SIAM J. Comput., 43(3):1012-1063, 2014. URL: https://doi.org/10.1137/120900095.
  20. Emanuel Kieronski and Martin Otto. Small substructures and decidability issues for first-order logic with two variables. J. Symb. Log., 77(3):729-765, 2012. URL: https://doi.org/10.2178/jsl/1344862160.
  21. Emanuel Kieronski, Ian Pratt-Hartmann, and Lidia Tendera. Equivalence closure in the two-variable guarded fragment. J. Log. Comput., 27(4):999-1021, 2017. URL: https://doi.org/10.1093/logcom/exv075.
  22. Emanuel Kieronski and Sebastian Rudolph. Finite model theory of the triguarded fragment and related logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470734.
  23. Emanuel Kieronski and Lidia Tendera. Finite satisfiability of the two-variable guarded fragment with transitive guards and related variants. ACM Trans. Comput. Log., 19(2):8:1-8:34, 2018. URL: https://doi.org/10.1145/3174805.
  24. Ian Pratt-Hartmann. Fragments of First-Order Logic. Oxford Logic Guides. Oxford University Press, United Kingdom, 2023. Google Scholar
  25. Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. Quine’s fluted fragment is non-elementary. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille, France, August 29 - September 1, 2016, volume 62 of LIPIcs, pages 39:1-39:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.39.
  26. Riccardo Rosati. The limits of querying ontologies. In Thomas Schwentick and Dan Suciu, editors, Database Theory - ICDT 2007, 11th International Conference, Barcelona, Spain, January 10-12, 2007, Proceedings, volume 4353 of Lecture Notes in Computer Science, pages 164-178, Berlin, Heidelberg, 2007. Springer. URL: https://doi.org/10.1007/11965893_12.
  27. Sebastian Rudolph, Markus Krötzsch, and Pascal Hitzler. All elephants are bigger than all mice. In Franz Baader, Carsten Lutz, and Boris Motik, editors, Proceedings of the 21st International Workshop on Description Logics (DL2008), Dresden, Germany, May 13-16, 2008, volume 353 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. URL: https://ceur-ws.org/Vol-353/RudolphKraetzschHitzler.pdf.
  28. Sebastian Rudolph and Mantas Simkus. The triguarded fragment of first-order logic. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, volume 57 of EPiC Series in Computing, pages 604-619. EasyChair, 2018. URL: https://doi.org/10.29007/m8ts.
  29. Larry J. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Massachusetts Institute of Technology, USA, Cambridge, Massasuchets, USA, 1974. URL: http://hdl.handle.net/1721.1/15540.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact