  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 succesful for positive
query languages (such a unions of conjunctive queries, positive relational
algebra, or 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.
