Provenance Analysis and Semiring Semantics for First-Order Logic

TL;DR

This paper extends provenance analysis to full first-order logic with negation using quotient semirings, enabling explanation of query results, failures, and repairs, and advancing semiring semantics in logic.

Contribution

It introduces a novel semiring provenance framework for first-order logic with negation, allowing reverse analysis and broadening applications.

Findings

Provenance analysis now applicable to full first-order logic with negation.

Enables reverse provenance analysis to find models satisfying properties.

Potential applications include explaining query failures and computing repairs.

Abstract

A provenance analysis for a query evaluation or a model checking computation extracts information on how its result depends on the atomic facts of the model or database. Traditional work on data provenance was, to a large extent, restricted to positive query languages or 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. We describe and evaluate here a provenance approach for dealing with negation, based on quotient semirings of polynomials with dual indeterminates. This not only provides a semiring provenance analysis for full first-order logic (and other logics and query languages with negation) but also permits a reverse provenance analysis, i.e., finding models that satisfy various properties under given provenance tracking assumptions. We describe the potential for applications to explaining missing query answers or failures of integrity constraints, and to using these explanations for computing repairs. This approach also is the basis of a systematic study of semiring semantics in a broad logical context.