# Semiring Provenance for First-Order Model Checking

arXiv: https://arxiv.org/abs/1712.01980 · HTML: https://mlsanity.com/paper/1712.01980/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Dec 2017.

## Built on by (most cited first, 1 of 1)

- [Shape Fragments](https://mlsanity.com/paper/2112.11796/) (2021)

## Abstract (arXiv)

Given a first-order sentence, a model-checking computation tests whether the sentence holds true in a given finite structure. Data provenance extracts from this computation an abstraction of the manner in which its result depends on the data items that describe the model. Previous work on provenance was, to a large extent, restricted to the negation-free fragment of first-order logic and showed how provenance abstractions can be usefully described as elements of commutative semirings --- most generally as multivariate polynomials with positive integer coefficients. In this paper we introduce a novel approach to dealing with negation and a corresponding commutative semiring of polynomials with dual indeterminates. These polynomials are used to perform reverse provenance analysis, i.e., finding models that satisfy various properties under given provenance tracking assumptions.