Document Open Access Logo

On Homogeneous Models of Fluted Languages

Author Daumantas Kojelis

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.9.pdf
  • Filesize: 0.88 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • Fluted Fragment
  • Fluted Logic
  • Fluted Fragment with Periodic Counting
  • Adjacent Fragment
  • Adjacent Fragment with Counting
  • Adjacent Fragment with Periodic Counting
  • Counting Quantifiers
  • Periodic Counting Quantifiers
  • Decidable Fragments of First-Order Logic

Metrics

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

Abstract

We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of "nice" models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is Tower-complete. If only two variable are used, computational complexity drops to NExpTime-completeness. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have finite and general satisfiability problems which are, respectively, Σ⁰₁- and Π⁰₁-complete. Additionally, satisfiability becomes Σ¹₁-complete if periodic counting quantifiers are permitted.

Cite As Get BibTex

Daumantas Kojelis. On Homogeneous Models of Fluted Languages. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.9

Author Details

Daumantas Kojelis
  • Department of Computer Science, University of Manchester, UK

Funding

This work is supported by the NCN grant 2018/31/B/ST6/03662.

Acknowledgements

The author would like to thank Dr. Ian Pratt-Hartmann and Dr. Bartosz Jan Bednarczyk for their valuable feedback.

References

  1. Franz Baader. A new description logic with set constraints and cardinality constraints on role successors. In Frontiers of Combining Systems, pages 43-59. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-66167-4_3.
  2. Bartosz Bednarczyk. Exploiting forwardness: Satisfiability and query-entailment in forward guarded fragment. In 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 and Reijo Jaakkola. Towards a model theory of ordered logics: Expressivity and interpolation. In 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.
  4. 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), volume 261 of Leibniz International Proceedings in Informatics (LIPIcs), pages 111:1-111:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.111.
  5. Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, and Tony Tan. On Classical Decidable Logics Extended with Percentage Quantifiers and Arithmetics. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), volume 213 of Leibniz International Proceedings in Informatics (LIPIcs), pages 36:1-36:15, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2021.36.
  6. Michael Benedikt, Egor V. Kostylev, and Tony Tan. Two variable logic with ultimately periodic counting. SIAM Journal on Computing, 53(4):884-968, 2024. URL: https://doi.org/10.1137/22M1504792.
  7. Erich Grädel, Martin Otto, and Eric Rosen. Undecidability results on two-variable logics. Archive for Mathematical Logic, 38(4):313-354, 1999. URL: https://doi.org/10.1007/S001530050130.
  8. Erich Grädel. On the restraining power of guards. The Journal of Symbolic Logic, 64(4):1719-1742, 1999. URL: https://doi.org/10.2307/2586808.
  9. 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: https://doi.org/10.2307/421196.
  10. David Harel. Recurring dominoes: Making the highly undecidable highly understandable. In Topics in the Theory of Computation, volume 102 of North-Holland Mathematics Studies, pages 51-71. North-Holland, 1985. Google Scholar
  11. 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, 1990. Google Scholar
  12. 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
  13. Reijo Jaakkola. Ordered fragments of first-order logic. In 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.
  14. Emil Jeřábek. Division by zero. Archive for Mathematical Logic, 55(7):997-1013, 2016. URL: https://doi.org/10.1007/S00153-016-0508-5.
  15. H. Jerome. Keisler. Model theory for infinitary logic : logic with countable conjunctions and finite quantifiers. Studies in logic and the foundations of mathematics ; v. 62. North-Holland Pub. Co., Amsterdam, 1971. Google Scholar
  16. Viktor Kuncak and Martin Rinard. Towards efficient satisfiability checking for boolean algebra with presburger arithmetic. In Automated Deduction - CADE-21, pages 215-230, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-73595-3_15.
  17. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, 1981. URL: https://doi.org/10.1145/322276.322287.
  18. Ian Pratt-Hartmann. The two-variable fragment with counting revisited. In 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.
  19. Ian Pratt-Hartmann. Fluted logic with counting. In 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.
  20. Ian Pratt-Hartmann. Fragments of First-Order Logic. Oxford University Press, 2023. Google Scholar
  21. Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. The fluted fragment revisited. Journal of Symbolic Logic, 84(3):1020-1048, 2019. URL: https://doi.org/10.1017/JSL.2019.33.
  22. Ian Pratt-Hartmann and Lidia Tendera. The Fluted Fragment with Transitivity. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.MFCS.2019.18.
  23. 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.
  24. Ian Pratt-Hartmann and Lidia Tendera. Adding Transitivity and Counting to the Fluted Fragment. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 32:1-32:22, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.CSL.2023.32.
  25. William C. Purdy. Fluted formulas and the limits of decidability. The Journal of Symbolic Logic, 61(2):608-620, 1996. URL: https://doi.org/10.2307/2275678.
  26. 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
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact