Ehrenfeucht-Fra\"iss\'e 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\"iss\'e 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\"iss\'e games but also for other variants based on bijections or counting. Finally we propose a new kind of games, called homomorphism games, which are based on the fact that there exist certain rather simple semiring interpretations that are locally very different and can be separated even in a one-move game, but which can be proved to be elementarily equivalent via separating sets of homomorphisms into the Boolean semiring. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite and infinite lattice semirings.

翻译：埃伦费赫特-弗雷瑟博弈是证明关系结构初等等价（以及特定量词秩下的等价性）的基本方法。我们在半环语义这一更一般的语境下研究该方法的可靠性与完备性。半环语义最初源于数据库查询的溯源分析，它并非仅以真或假来评估逻辑语句，而是通过某个交换半环中的值进行评估；这能够提供更详尽的信息，例如蕴含语句真值的原子事实组合，或关于评估代价、置信度得分、访问级别或成功评估策略数量的实用信息。与溯源分析相关的半环种类繁多，而经典逻辑方法在半环语义中的适用性可能强烈依赖于底层半环的代数性质。尽管埃伦费赫特-弗雷瑟博弈在经典语义（即布尔半环）下对于逻辑等价性既是可靠也是完备的，但一般而言，在其他半环上情况并非如此。我们详细分析了特定半环上模型比较博弈的可靠性与完备性，不仅针对经典埃伦费赫特-弗雷瑟博弈，还针对基于双射或计数的其他变体。最后，我们提出一种新型博弈，称为同态博弈，其基于如下事实：存在某些相当简单的半环解释，它们在局部上差异显著，甚至可通过一步博弈加以区分，但可证明通过分离到布尔半环的同态集合而初等等价。我们证明了这些同态博弈在有限与无限格半环上为逻辑等价性提供了可靠且完备的方法。