Document Open Access Logo

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

Authors Neta Elad , Sharon Shoham

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.40.pdf
  • Filesize: 1.08 MB
  • 27 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • first-order logic
  • decidability
  • symbolic structures

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.LICS.2026.40

Author Details

Neta Elad
  • Tel Aviv University, Israel
Sharon Shoham
  • Tel Aviv University, Israel

Funding

The research leading to these results has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation programme (grant agreement No [759102-SVIS]). This research was partially supported by Israel Science Foundation (ISF) grant No. 2117/23.

References

  1. Aharon Abadi, Alexander Rabinovich, and Mooly Sagiv. Decidable fragments of many-sorted logic. J. Symb. Comput., 45(2):153-172, 2010. URL: https://doi.org/10.1016/j.jsc.2009.03.003.
  2. Wilhelm Ackermann. Über die erfüllbarkeit gewisser zählausdrücke. Mathematische Annalen, 100(1):638-649, 1928. URL: https://doi.org/10.1007/BF01448869.
  3. Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In Handbook of Automated Reasoning, pages 19-99. Elsevier and MIT Press, Amsterdam, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50004-7.
  4. Vince Bárány, Erich Grädel, and Sasha Rubin. Automata-based presentations of infinite structures. In Finite and Algorithmic Model Theory, volume 379 of London Mathematical Society Lecture Note Series, pages 1-76. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511974960.002.
  5. Vince Bárány, Balder ten Cate, and Luc Segoufin. Guarded negation. In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 356-367, Berlin, Germany, 2011. Springer. URL: https://doi.org/10.1007/978-3-642-22012-8_28.
  6. Michael Benedikt, Leonid Libkin, Thomas Schwentick, and Luc Segoufin. Definable relations and first-order query languages over strings. J. ACM, 50(5):694-751, 2003. URL: https://doi.org/10.1145/876638.876642.
  7. Achim Blumensath and Erich Grädel. Finite presentations of infinite structures: Automata and interpretations. Theory Comput. Syst., 37(6):641-674, 2004. URL: https://doi.org/10.1007/S00224-004-1133-Y.
  8. Achim Blumensath and Erich Grädel. Finite presentations of infinite structures: Automata and interpretations. Theory Comput. Syst., 37(6):641-674, 2004. URL: https://doi.org/10.1007/s00224-004-1133-y.
  9. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Berlin, 1997. Google Scholar
  10. J Richard Büchi. On a decision method in restricted second order arithmetic. In The Collected Works of J. Richard Büchi, pages 425-435. Springer New York, New York, NY, 1990. Google Scholar
  11. J. Richard Büchi and Lawrence H. Landweber. Definability in the monadic second-order theory of successor. J. Symb. Log., 34(2):166-170, 1969. URL: https://doi.org/10.2307/2271090.
  12. David C Cooper. Theorem proving in arithmetic without multiplication. Machine intelligence, 7(91-99):300, 1972. URL: https://doi.org/10.1007/10930755_5.
  13. Daniel Danielski and Emanuel Kieronski. Finite satisfiability of unary negation fragment with transitivity. In MFCS, volume 138 of LIPIcs, pages 17:1-17:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.17.
  14. Neta Elad. Infinite models tools (FEST). https://www.cs.tau.ac.il/~netaelad/#infinite-models-fest. Accessed: 2024-05-06.
  15. Neta Elad, Oded Padon, and Sharon Shoham. An infinite needle in a finite haystack: Finding infinite counter-models in deductive verification. Proc. ACM Program. Lang., 8(POPL):970-1000, 2024. URL: https://doi.org/10.1145/3632875.
  16. Neta Elad and Sharon Shoham. Decidability results for fragments of first-order logic via a symbolic model property, 2026. URL: https://arxiv.org/abs/2605.05840.
  17. Kurt Gödel. Ein spezialfall des entscheidungsproblems der theoretischen logik. Ergebnisse eines mathematischen Kolloquiums, 2:27-28, 1932. Google Scholar
  18. Erich Grädel, Wied Pakusa, Svenja Schalthöfer, and Lukasz Kaiser. Characterising choiceless polynomial time with first-order interpretations. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 677-688. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.68.
  19. Yuri Gurevich. The decision problem for standard classes. The Journal of Symbolic Logic, 41(2):460-464, 1976. URL: https://doi.org/10.1017/S0022481200051513.
  20. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, and Mooly Sagiv. Effectively-propositional reasoning about reachability in linked data structures. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 756-772, Berlin, Germany, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-39799-8_53.
  21. László Kalmár. Über die erfüllbarkeit derjenigen zählausdrücke, welche in der normalform zwei benachbarte allzeichen enthalten. Mathematische Annalen, 108(1):466-484, 1933. Google Scholar
  22. Bakhadyr Khoussainov and Anil Nerode. Automatic presentations of structures. In Daniel Leivant, editor, Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, Indiana, USA, 13-16 October 1994, volume 960 of Lecture Notes in Computer Science, pages 367-392. Springer, 1994. URL: https://doi.org/10.1007/3-540-60178-3_93.
  23. Nils Klarlund and Anders Møller. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, January 2001. Notes Series NS-01-1. Available from URL: http://www.brics.dk/mona/.
  24. Harry R. Lewis. Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci., 21(3):317-353, 1980. URL: https://doi.org/10.1016/0022-0000(80)90027-6.
  25. Martin Löb. Decidability of the monadic predicate calculus with unary function symbols. Journal of Symbolic Logic, 32(4):563, 1967. Google Scholar
  26. Giuliano Losa and Mike Dodds. On the formal verification of the stellar consensus protocol. In Bruno Bernardo and Diego Marmsoler, editors, 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, Los Angeles, California, USA (Virtual Conference), July 20-21, 2020, volume 84 of OASIcs, pages 9:1-9:9, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.FMBC.2020.9.
  27. Raz Lotan and Sharon Shoham. Implicit rankings for verifying liveness properties in first-order logic. In Arie Gurfinkel and Marijn Heule, editors, Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I, volume 15696 of Lecture Notes in Computer Science, pages 375-395, Berlin, Germany, 2025. Springer. URL: https://doi.org/10.1007/978-3-031-90643-5_20.
  28. Kenneth L. McMillan and Oded Padon. Deductive verification in decidable fragments with ivy. In Andreas Podelski, editor, Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, volume 11002 of Lecture Notes in Computer Science, pages 43-55, Berlin, Germany, 2018. Springer. URL: https://doi.org/10.1007/978-3-319-99725-4_4.
  29. Michael Mortimer. On languages with two variables. Mathematical Logic Quarterly, 21(1):135-140, 1975. URL: https://doi.org/10.1002/malq.19750210118.
  30. Adithya Murali, Lucas Peña, Ranjit Jhala, and P. Madhusudan. Complete first-order reasoning for properties of functional programs. Proc. ACM Program. Lang., 7(OOPSLA2):1063-1092, 2023. URL: https://doi.org/10.1145/3622835.
  31. Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang., 1(OOPSLA):108:1-108:31, 2017. URL: https://doi.org/10.1145/3140568.
  32. Nicolas Peltier. Building infinite models for equational clause sets: Constructing non-ambiguous formulae. Log. J. IGPL, 11(1):97-129, 2003. URL: https://doi.org/10.1093/jigpal/11.1.97.
  33. Michael O Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society, 141:1-35, 1969. URL: https://doi.org/10.2307/1995086.
  34. Frank P Ramsey. On a problem of formal logic. Procedures of London Mathematical Society, 30:264-285, 1930. URL: https://doi.org/10.1007/978-0-8176-4842-8_1.
  35. Saharon Shelah. Decidability of a portion of the predicate calculus. Israel Journal of Mathematics, 28(1):32-44, 1977. URL: https://doi.org/10.1007/BF02759780.
  36. Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, and Mooly Sagiv. Counterexample driven quantifier instantiations with applications to distributed protocols. Proc. ACM Program. Lang., 7(OOPSLA2):1878-1904, 2023. URL: https://doi.org/10.1145/3622864.
  37. Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. Modularity for decidability of deductive verification with applications to distributed systems. In Jeffrey S. Foster and Dan Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 662-677, New York, NY, 2018. ACM. URL: https://doi.org/10.1145/3192366.3192414.
  38. Marco Voigt. Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates. PhD thesis, Saarland University, Saarbrücken, Germany, 2019. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/27767.
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