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.

翻译：查询求值或模型检验计算的溯源分析旨在提取结果如何依赖于模型或数据库原子事实的信息。传统的数据溯源研究在很大程度上局限于正查询语言或一阶逻辑的无否定片段，并证明了溯源抽象可被有效地描述为交换半环中的元素——最一般地表示为具有正整数系数的多元多项式。本文提出并评估了一种基于具有对偶未定元的多项式商半环来处理否定的溯源方法。这不仅为完整一阶逻辑（以及其他具有否定的逻辑和查询语言）提供了半环溯源分析，还支持逆向溯源分析，即在给定溯源追踪假设下寻找满足特定性质的模型。我们阐述了该方法在解释缺失查询答案或完整性约束失效方面的应用潜力，以及如何利用这些解释进行修复计算。此方法也为在广泛逻辑语境下系统研究半环语义奠定了基础。