DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.40

Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property

Authors: Neta Elad and Sharon Shoham

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

Abstract

Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize symbolic structures to use any base theory that admits a standard model. Symbolic structures induce a symbolic model property, which holds for a fragment of first-order logic if every satisfiable formula in the fragment has a symbolic model. The symbolic model property implies decidability, since the model-checking problem for symbolic structures is decidable. We use the symbolic model property to prove decidability for several fragments that extend the fragment of stratified formulas, relaxing the quantifier-alternation constraints by allowing one sort to have self-looping functions, under certain restrictions. To establish the symbolic model property for these fragments we construct a symbolic model for a formula from an arbitrary model. The construction and its correctness are proved in a generic fashion, which may be instantiated to other similarly restricted fragments.

Cite as

Neta Elad and Sharon Shoham. Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 40:1-40:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{elad_et_al:LIPIcs.LICS.2026.40,
  author =	{Elad, Neta and Shoham, Sharon},
  title =	{{Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{40:1--40:27},
  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.40},
  URN =		{urn:nbn:de:0030-drops-268274},
  doi =		{10.4230/LIPIcs.LICS.2026.40},
  annote =	{Keywords: first-order logic, decidability, symbolic structures}
}

Search Results

Documents authored by Elad, Neta

Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property

Abstract

Cite as

Thanks for your feedback!

Could not send message