A model-checking computation checks whether a given logical sentence is
true in a given finite structure. Provenance analysis abstracts from such a
computation mathematical information on how the result depends on the atomic
data that describe the structure. In database theory, provenance analysis by
interpretations in commutative semirings has been rather successful for positive
query languages (such as unions of conjunctive queries, positive relational algebra,
and Datalog). However, it did not really offer an adequate treatment of
negation or missing information. Here we propose a new approach for the
provenance analysis of logics with negation, such as first-order logic and
fixed-point logics. It is closely related to a provenance analysis of the associated
model-checking games, and based on new semirings of dual-indeterminate
polynomials or dual-indeterminate formal power series. These are obtained by taking
quotients of traditional provenance semirings by congruences that are generated
by products of positive and negative provenance tokens. Beyond the use
for model-checking problems in logics, provenance analysis of games is of
independent interest. Provenance values in games provide detailed information
about the number and properties of the strategies of the players, far beyond
the question whether or not a player has a winning strategy from a given
position.
