Vol. 9, No. 3, 2020

Download this article
Download this article For screen
For printing
Recent Issues
Volume 12, Issue 1
Volume 11, Issue 4
Volume 11, Issue 3
Volume 11, Issue 2
Volume 11, Issue 1
Volume 10, Issue 4
Volume 10, Issue 3
Volume 10, Issue 2
Volume 10, Issue 1
Volume 9, Issue 4
Volume 9, Issue 3
Volume 9, Issue 2
Volume 9, Issue 1
Volume 8, Issue 4
Volume 8, Issue 3
Volume 8, Issue 2
Volume 8, Issue 1
Older Issues
Volume 7, Issue 4
Volume 7, Issue 3
Volume 7, Issue 2
Volume 7, Issue 1
Volume 6, Issue 4
Volume 6, Issue 2-3
Volume 6, Issue 1
Volume 5, Issue 4
Volume 5, Issue 3
Volume 5, Issue 1-2
Volume 4, Issue 4
Volume 4, Issue 3
Volume 4, Issue 2
Volume 4, Issue 1
Volume 3, Issue 3-4
Volume 3, Issue 2
Volume 3, Issue 1
Volume 2, Issue 4
Volume 2, Issue 3
Volume 2, Issue 2
Volume 2, Issue 1
Volume 1, Issue 4
Volume 1, Issue 3
Volume 1, Issue 2
Volume 1, Issue 1
The Journal
About the Journal
Editorial Board
Submission Guidelines
Submission Form
Policies for Authors
Ethics Statement
founded and published with the
scientific support and advice of
mathematicians from the
Moscow Institute of
Physics and Technology
ISSN (electronic): 2640-7361
ISSN (print): 2220-5438
Author Index
To Appear
Other MSP Journals
Provenance analysis for logic and games

Erich Grädel and Val Tannen

Vol. 9 (2020), No. 3, 203–228

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.

finite model theory, semiring provenance, games
Mathematical Subject Classification 2010
Primary: 03B70, 03C13, 05C57, 68Q19, 91A43
Received: 2 August 2019
Accepted: 21 February 2020
Published: 15 October 2020
Erich Grädel
RWTH Aachen University
Val Tannen
University of Pennsylvania
Philadelphia, PA
United States