DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.44

The Guarded Fragment with Nested Equivalences

Authors: Oskar Fiuk

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{fiuk:LIPIcs.LICS.2026.44,
  author =	{Fiuk, Oskar},
  title =	{{The Guarded Fragment with Nested Equivalences}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{44:1--44:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.44},
  URN =		{urn:nbn:de:0030-drops-268313},
  doi =		{10.4230/LIPIcs.LICS.2026.44},
  annote =	{Keywords: guarded fragment, finite model property, nested equivalence relations}
}

Document

DOI: 10.4230/LIPIcs.STACS.2026.37

Random Models and Guarded Logic

Authors: Oskar Fiuk

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract

Building on ideas of Gurevich and Shelah for the Gödel Class, we present a new probabilistic proof of the finite model property for the Guarded Fragment of First-Order Logic. Our proof is conceptually simple and yields the optimal doubly-exponential upper bound on the size of minimal models. We precisely analyse the obtained bound, up to constant factors in the exponents, and construct sentences that enforce models of tightly matching size. The probabilistic approach adapts naturally to the Triguarded Fragment, an extension of the Guarded Fragment that also subsumes the Two-Variable Fragment. Finally, we derandomise the probabilistic proof by providing an explicit model construction which replaces randomness with deterministic hash functions.

Cite as

Oskar Fiuk. Random Models and Guarded Logic. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fiuk:LIPIcs.STACS.2026.37,
  author =	{Fiuk, Oskar},
  title =	{{Random Models and Guarded Logic}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{37:1--37:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.37},
  URN =		{urn:nbn:de:0030-drops-255269},
  doi =		{10.4230/LIPIcs.STACS.2026.37},
  annote =	{Keywords: guarded fragment, finite model property, probabilistic method}
}

Search Results

Documents authored by Fiuk, Oskar

The Guarded Fragment with Nested Equivalences

Abstract

Cite as

Random Models and Guarded Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message