Document Open Access Logo

Locality Theorems in Semiring Semantics

Authors Clotilde Bizière, Erich Grädel , Matthias Naaf

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2023.20.pdf
  • Filesize: 0.72 MB
  • 15 pages

Document Identifiers

Author Details

Clotilde Bizière
  • ENS Paris, France
Erich Grädel
  • RWTH Aachen University, Germany
Matthias Naaf
  • RWTH Aachen University, Germany

Cite As Get BibTex

Clotilde Bizière, Erich Grädel, and Matthias Naaf. Locality Theorems in Semiring Semantics. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.MFCS.2023.20

Abstract

Semiring semantics of first-order logic generalises classical Boolean semantics by permitting truth values from a commutative semiring, which can model information such as costs or access restrictions. This raises the question to what extent classical model-theoretic properties still apply, and how this depends on the algebraic properties of the semiring.
In this paper, we study this question for the classical locality theorems due to Hanf and Gaifman. We prove that Hanf’s locality theorem generalises to all semirings with idempotent operations, but fails for many non-idempotent semirings. We then consider Gaifman normal forms and show that for formulae with free variables, Gaifman’s theorem does not generalise beyond the Boolean semiring. Also for sentences, it fails in the natural semiring and the tropical semiring. Our main result, however, is a constructive proof of the existence of Gaifman normal forms for min-max and lattice semirings. The proof implies a stronger version of Gaifman’s classical theorem in Boolean semantics: every sentence has a Gaifman normal form which does not add negations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • Semiring semantics
  • Locality
  • First-order logic

Metrics

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

Related Versions

References

  1. M. Arenas, P. Barceló, and L. Libkin. Game-based notions of locality over finite models. Ann. Pure Appl. Log., 152(1-3):3-30, 2008. URL: https://doi.org/10.1016/j.apal.2007.11.012.
  2. M. Benedikt, T. Griffin, and L. Libkin. Verifiable properties of database transactions. Inf. Comput., 147(1):57-88, 1998. URL: https://doi.org/10.1006/inco.1998.2731.
  3. S. van Bergerem. Learning concepts definable in first-order logic with counting. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1-13, 2019. URL: https://doi.org/10.1109/LICS.2019.8785811.
  4. S. van Bergerem, M. Grohe, and M. Ritzert. On the parameterized complexity of learning first-order logic. In PODS '22: International Conference on Management of Data, pages 337-346. ACM, 2022. URL: https://doi.org/10.1145/3517804.3524151.
  5. S. van Bergerem and N. Schweikardt. Learning concepts described by weight aggregation logic. In 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, pages 10:1-10:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.10.
  6. C. Bizière, E. Grädel, and M. Naaf. Locality theorems in semiring semantics, 2023. Full version of this paper. URL: https://arxiv.org/abs/2303.12627.
  7. S. Brinke. Ehrenfeucht-Fraïssé Games for Semiring Semantics. M. Sc. thesis, RWTH Aachen University, 2023. URL: https://logic.rwth-aachen.de/pub/brinke/masterarbeit.pdf.
  8. A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt. Approximation schemes for first-order definable optimisation problems. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pages 411-420. IEEE, 2006. URL: https://doi.org/10.1109/LICS.2006.13.
  9. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer, 2nd edition, 1995. URL: https://doi.org/10.1007/3-540-28788-4.
  10. J. Foster, T. Green, and V. Tannen. Annotated XML: queries and provenance. In Proceedings of PODS, pages 271-280, 2008. URL: https://doi.org/10.1145/1376916.1376954.
  11. H. Gaifman. On local and non-local properties. In J. Stern, editor, Proceedings of the Herbrand Symposium, volume 107 of Studies in Logic and the Foundations of Mathematics, pages 105-135. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(08)71879-2.
  12. B. Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209-441, 2021. URL: https://doi.org/10.1561/1900000068.
  13. E. Grädel, H. Helal, M. Naaf, and R. Wilke. Zero-one laws and almost sure valuations of first-order logic in semiring semantics. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 41:1-41:12. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533358.
  14. E. Grädel, N. Lücking, and M. Naaf. Semiring provenance for Büchi games: Strategy analysis with absorptive polynomials. In Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021), volume 346 of EPTCS, pages 67-82, 2021. URL: https://doi.org/10.4204/EPTCS.346.5.
  15. E. Grädel and L. Mrkonjić. Elementary equivalence versus isomorphism in semiring semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198, pages 133:1-133:20, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.133.
  16. E. Grädel and V. Tannen. Semiring provenance for first-order model checking, 2017. URL: https://arxiv.org/abs/1712.01980.
  17. E. Grädel and V. Tannen. Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory, 9(3):203-228, 2020. URL: https://doi.org/10.2140/moscow.2020.9.203.
  18. T. Green and V. Tannen. The semiring framework for database provenance. In Proceedings of PODS, pages 93-99. ACM, 2017. URL: https://doi.org/10.1145/3034786.3056125.
  19. M. Grohe, S. Kreutzer, and S. Siebertz. Deciding first-order properties of nowhere dense graphs. J. ACM, 64(3):17:1-17:32, 2017. URL: https://doi.org/10.1145/3051095.
  20. M. Grohe and S. Wöhrle. An existential locality theorem. Ann. Pure Appl. Log., 129(1-3):131-148, 2004. URL: https://doi.org/10.1016/j.apal.2004.01.005.
  21. L. Hella, L. Libkin, and J. Nurmonen. Notions of locality and their logical characterizations over finite models. J. Symb. Log., 64(4):1751-1773, 1999. URL: https://doi.org/10.2307/2586810.
  22. L. Hella, L. Libkin, J. Nurmonen, and L. Wong. Logics with aggregate operators. J. ACM, 48(4):880-907, 2001. URL: https://doi.org/10.1145/502090.502100.
  23. D. Kuske and N. Schweikardt. Gaifman normal forms for counting extensions of first-order logic. In 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, July 9-13, 2018, Prague, Czech Republic, volume 107 of LIPIcs, pages 133:1-133:14, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.133.
  24. L. Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07003-1.
  25. T. Schwentick and K. Barthelmann. Local normal forms for first-order logic with applications to games and automata. In STACS 98, 15th Annual Symposium on Theoretical Aspects of Computer Science, Paris, France, February 25-27, 1998, Proceedings, volume 1373 of Lecture Notes in Computer Science, pages 444-454. Springer, 1998. URL: https://doi.org/10.1007/BFb0028580.
  26. J. Xu, W. Zhang, A. Alawini, and V. Tannen. Provenance analysis for missing answers and integrity repairs. IEEE Data Eng. Bull., 41(1):39-50, 2018. URL: http://sites.computer.org/debull/A18mar/p39.pdf.
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact