Vol. 9, No. 3, 2020

Download this article
Download this article For screen
For printing
Recent Issues
Volume 13, Issue 1
Volume 12, Issue 4
Volume 12, Issue 3
Volume 12, Issue 2
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
ISSN (electronic): 2996-220X
ISSN (print): 2996-2196
Author Index
To Appear
Other MSP Journals
This article is available for purchase or by subscription. See below.
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.

PDF Access Denied

We have not been able to recognize your IP address as that of a subscriber to this journal.
Online access to the content of recent issues is by subscription, or purchase of single articles.

Please contact your institution's librarian suggesting a subscription, for example by using our journal-recom­mendation form. Or, visit our subscription page for instructions on purchasing a subscription.

You may also contact us at contact@msp.org
or by using our contact form.

Or, you may purchase this single article for USD 40.00:

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