Ehrenfeucht-Fraïssé Games in Semiring Semantics

Authors Sophie Brinke , Erich Grädel , Lovro Mrkonjić

Thumbnail PDF


  • Filesize: 0.79 MB
  • 22 pages

Document Identifiers

Author Details

Sophie Brinke
  • RWTH Aachen University, Germany
Erich Grädel
  • RWTH Aachen University, Germany
Lovro Mrkonjić
  • RWTH Aachen University, Germany

Cite AsGet BibTex

Sophie Brinke, Erich Grädel, and Lovro Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Ehrenfeucht-Fraïssé games provide a fundamental method for proving elementary equivalence (and equivalence up to a certain quantifier rank) of relational structures. We investigate the soundness and completeness of this method in the more general context of semiring semantics. Motivated originally by provenance analysis of database queries, semiring semantics evaluates logical statements not just by true or false, but by values in some commutative semiring; this can provide much more detailed information, for instance concerning the combinations of atomic facts that imply the truth of a statement, or practical information about evaluation costs, confidence scores, access levels or the number of successful evaluation strategies. There is a wide variety of different semirings that are relevant for provenance analysis, and the applicability of classical logical methods in semiring semantics may strongly depend on the algebraic properties of the underlying semiring. While Ehrenfeucht-Fraïssé games are sound and complete for logical equivalences in classical semantics, and thus on the Boolean semiring, this is in general not the case for other semirings. We provide a detailed analysis of the soundness and completeness of model comparison games on specific semirings, not just for classical Ehrenfeucht-Fraïssé games but also for other variants based on bijections or counting. Finally we propose a new kind of games, called homomorphism games, based on the fact that there exist locally very different semiring interpretations that can be proved to be elementarily equivalent via separating sets of homomorphisms. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite lattice semirings.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Semiring semantics
  • elementary equivalence
  • Ehrenfeucht-Fraïssé games


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


  1. Garrett Birkhoff. Lattice Theory. American Mathematical Society, Providence, 3rd edition, 1967. Google Scholar
  2. 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), volume 272 of LIPIcs, pages 20:1-20:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL:
  3. Camille Bourgaux, Ana Ozaki, Rafael Peñaloza, and Livia Predoiu. Provenance for the description logic ELHr. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI 2020), pages 1862-1869., 2020. URL:
  4. Sophie Brinke, Erich Grädel, and Lovro Mrkonjić. Ehrenfeucht-Fraïssé games in semiring semantics, 2023. Full version of this paper. URL:
  5. Katrin Dannert and Erich Grädel. Provenance analysis: A perspective for description logics? In Description Logic, Theory Combination, and All That, volume 11560 of Lecture Notes in Computer Science, pages 266-285. Springer, 2019. URL:
  6. Katrin Dannert and Erich Grädel. Semiring provenance for guarded logics. In Hajnal Andréka and István Németi on Unity of Science, volume 19 of Outstanding Contributions to Logic, pages 53-79. Springer, Cham, 2021. URL:
  7. Katrin Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. Semiring provenance for fixed-point logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of LIPIcs, pages 17:1-17:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL:
  8. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer, 2nd edition, 1995. URL:
  9. Boris Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209-441, 2021. URL:
  10. Erich Grädel, Hayyan Helal, Matthias Naaf, and Richard Wilke. Zero-one laws and almost sure valuations of first-order logic in semiring semantics. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022), pages 41:1-41:12. ACM, 2022. URL:
  11. Erich Grädel, Niels Lücking, and Matthias 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:
  12. Erich Grädel and Lovro Mrkonjić. Elementary equivalence versus isomorphism in semiring semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198 of LIPIcs, pages 133:1-133:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL:
  13. Erich Grädel and Val Tannen. Semiring provenance for first-order model checking, 2017. URL:
  14. Erich Grädel and Val Tannen. Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory, 9(3):203-228, 2020. URL:
  15. Todd J. Green, Grigoris Karvounarakis, and Val Tannen. Provenance semirings. In Proceedings of the Twenty-Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS 2007), pages 31-40. ACM, 2007. URL:
  16. Todd J. Green and Val Tannen. The semiring framework for database provenance. In Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2017), pages 93-99. ACM, 2017. URL:
  17. Lauri Hella. Logical hierarchies in PTIME. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS 1992), pages 360-368. IEEE Computer Society, 1992. URL:
  18. Neil Immerman and Eric Lander. Describing graphs: A first-order approach to graph canonization. In Complexity Theory Retrospective, pages 59-81. Springer, New York, 1990. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail