Pith. sign in

REVIEW 1 major objections 5 minor 44 references

Provenance Analysis and Semiring Semantics for First-Order Logic

T0 review · 1 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Full first-order logic gains a provenance semantics: every sentence maps to a polynomial that catalogs its proof trees.

desk verdict Solid consolidation of the authors' own 2017 framework; the proof-tree semantics and repair machinery are genuinely useful, novelty is limited but the paper earns a serious referee. read the letter →

arxiv 2412.07986 v1 pith:FCENPQDI submitted 2024-12-10 cs.LO cs.DB

Erich Grädel , Val Tannen This is my paper · ORCID
classification cs.LOcs.DB MSC 03B7068P15
keywords provenancesemanticssemiringfirst-orderlogicnegationdualindeterminatesprooftreesreversedatabaserepairs
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper extends semiring provenance, the practice of annotating data items with algebraic values so that a query's output tracks which input facts it depends on, from positive query languages to full first-order logic with negation. The key move is to evaluate sentences in a quotient semiring of polynomials whose indeterminates come in positive-negative pairs, with each token and its dual forced to multiply to zero. For any sentence and any model-compatible annotation of literals, the resulting polynomial lists every proof tree that verifies the sentence: each monomial stands for a family of distinct proof trees, and the polynomial is zero exactly when no proof tree exists. If this is right, model-checking with negation can be analyzed with the same tools that worked for positive queries, and the same polynomials support reverse provenance, explanations of missing answers and integrity-constraint failures, and repair computation.

What carries the argument

The central object is the semiring $\mathbb{N}[X,\bar X]$ of dual-indeterminate provenance polynomials: multivariate polynomials over two disjoint token sets $X$ and $\bar X$ in one-to-one correspondence, quotiented by $x\cdot\bar x=0$ for each complementary pair. A model-compatible interpretation annotates each literal with its own token, with 1 for facts accepted freely, or with 0 for absent facts, and never uses a token and its dual inconsistently for the same fact. The value of a sentence is built by interpreting disjunction and existential quantifiers as sums, conjunction and universal quantifiers as products over the finite universe, and negation by conversion to negation normal form. Theorem 1 — the value of any sentence equals the sum of the valuations of its evaluation trees — is what turns these polynomials into a complete census of proof trees, with dual tokens canceling exactly the trees that would rely on contradictory premises.

What would settle it

Choose a finite model-compatible interpretation, enumerate all evaluation trees of a sentence by brute force, and compare the coefficient of each monomial in $\mathcal{B}[\![\psi]\!]$ with the number of distinct proof trees using exactly those tracked literals; any mismatch would refute Theorem 2.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is Theorem 2: for any model-compatible interpretation $\mathcal{B}$ mapping literals to dual-indeterminate polynomials over paired tokens, and any first-order sentence $\psi$, the value $\mathcal{B}[\![\psi]\!]$ describes all proof trees that verify $\psi$ using premises that $\mathcal{B}$ maps to tokens or to 1. Each monomial $c\,x_1^{a_1}\cdots x_k^{a_k}$ corresponds to $c$ distinct proof trees using the annotated literals with the indicated multiplicities, and $\mathcal{B}[\![\psi]\!]\neq 0$ iff some proof tree exists. From this the paper derives Corollary 2: $\psi$ is $\mathrm{Mod}_{\mathcal{B}}$-satisfiable iff $\mathcal{B}[\![\psi]\!]\neq 0$, and $\psi$ is $\mathrm{Mod}_{\mathcal{B}}$-valid iff $\mathcal{B}[\![\neg\psi]\!]=0$. Specializing $\mathcal{B}$ to a particular model $\mathfrak{A}$ — setting to zero the tokens of literals false in $\mathfrak{A}$ — recovers the provenance of ordinary model-checking, while the unspecialized polynomial supports reverse analysis: each monomial identifies models compatible with the annotations that satisfy $\psi$, and solving $\mathcal{B}[\![\neg\psi]\!]=0$ yields repairs that make a failed query answer or integrity constraint true.

Load-bearing premise

The framework assumes a finite universe: quantifiers are evaluated as finite sums and products, so Theorem 2, reverse provenance, and repairs are stated for finite structures only.

Editorial extensions

If this is right

  • Full first-order logic, not just positive fragments, gets a uniform semiring provenance semantics, with negation handled without flattening to Boolean truth.
  • The monomials of $\mathcal{B}[\![\psi]\!]$ give a complete account of which combinations of positive and negative facts support the truth of $\psi$, and how many distinct proof trees each combination supports.
  • Reverse provenance becomes a by-product: $\mathcal{B}[\![\psi]\!]\neq 0$ decides satisfiability within the class of models compatible with the tracking assumptions, and $\mathcal{B}[\![\neg\psi]\!]=0$ decides validity within that class.
  • Missing query answers and integrity-constraint failures can be explained by the monomials of the provenance of the negated query, and minimal repairs are obtained by solving $\mathcal{B}[\![\neg\psi]\!]=0$, with costs or confidences then compared in other semirings.
  • Provenance can be updated after insertions and deletions by specializing one model-compatible polynomial, rather than recomputing from scratch.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If Theorem 2 holds, the same dual-indeterminate construction should transfer to any logic whose semantics is compositional over conjunction, disjunction, and quantifiers with negation in normal form, such as modal logics or description logics; the paper mentions such extensions elsewhere, and this is a direct extrapolation rather than a claim it tests.
  • The repair mechanism implicitly defines a cost-aware repair-selection procedure: once the model-compatible interpretation is fixed, choosing among repairs by tropical or Viterbi valuations is a single homomorphism evaluation, which suggests a practical pipeline for inconsistent databases that the paper illustrates but does not develop into an algorithm with guarantees.
  • The finiteness restriction is the real boundary of the theorem: on infinite universes the quantifier clauses would require infinitary semiring operations, so the proof-tree summation would need a different algebraic setting; the paper points to such extensions in related work, but the main claim here is finite-structure only.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper develops a semiring provenance semantics for full first-order logic with negation, based on quotient semirings of polynomials with dual indeterminates N[X,Xbar]. It defines S-interpretations over finite universes, proves a fundamental homomorphism property and a sum-of-proof-trees theorem, and then establishes a proof-tree characterization for model-compatible interpretations. From this it derives reverse provenance results, including restricted satisfiability and validity criteria, model specialization, update of provenance polynomials, and methods for explaining missing answers and computing repairs. The paper also surveys subsequent developments in semiring semantics for fixed-point logics, games, and model theory.

Significance. If the central claims hold, the paper fills a long-standing gap by extending provenance analysis from negation-free query languages to full first-order logic. The dual-indeterminate polynomial semiring is a concrete and natural construction, and the paper gives explicit, self-contained proofs of the main theorems plus worked examples showing how to obtain explanations, repairs, and confidence scores. The finite-universe restriction is stated clearly up front, and the proof-tree characterization in Theorem 2 is a strong, falsifiable claim. The paper also gives credit to the surrounding literature and spells out several applications.

major comments (1)
  1. [§4.1, Definition 6, Corollary 2] As written, Definition 6 does not require that different facts receive different provenance tokens, and §4.2 explicitly contemplates sharing the same token pair across several facts. Under that reading, Corollary 2 is false. Let the universe be {a,b}, let B(P(a)) = B(P(b)) = x and B(¬P(a)) = B(¬P(b)) = xbar, and let ψ = P(a) ∧ ¬P(b). Then B[[ψ]] = x · xbar = 0 in N[X,Xbar], yet the model with P(a) true and P(b) false is compatible with B and satisfies ψ. Thus the criterion 'ψ is Mod_B-satisfiable iff B[[ψ]] ≠ 0' fails. The same issue propagates to Corollary 3 and Proposition 16, where monomial variables are mapped back to individual facts. If the intended convention is that each token pair is reserved for exactly one ground literal, that injectivity condition should be stated explicitly in Definition 6, and the shared-token discussion in §4.2 should be reconciled with it.
minor comments (5)
  1. [§3.5] The definition of evaluation trees and proof trees only provides clauses for literals and the connectives ∧, ∨, ∃, ∀, while Theorem 1 is stated for every FO sentence. Please state explicitly that the theorem is applied to nnf(ψ), or extend the tree definition so that the root of an arbitrary FO formula is handled via Proposition 1.
  2. [§3.4, Proposition 7] The proof of Proposition 7 is only sketched: the induction measure is not stated and the literal base case is left implicit. Since the result is used to justify the 'consistency' discussion, a short explicit structural induction on NNF would make the argument easier to verify.
  3. [§4.3, Propositions 12 and 13] The complexity claims are asserted with 'a simple induction' and 'an examination of the proof' rather than proved. Given that the size model is a stated contribution, please expand these arguments or give precise bounds on the number of monomials.
  4. [§6] In the paragraph introducing the general model-compatible interpretation, the set 'D+ ∩ D−' appears to be a typo for 'D+ ∪ D−'; as written, the intersection is empty and the definition does not cover the intended updates.
  5. [§4.2 and §5.1] The notation for complementary tokens is not always consistent in the examples: sometimes a negative literal is annotated with 'x' and sometimes with 'xbar'. Using a uniform bar convention, as in the formal definition in §4.1, would prevent confusion.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central proof-tree characterization is derived by induction from independently defined proof trees, not assumed from the semantics or from prior self-citations.

full rationale

The paper's main derivation chain is self-contained. Definition 2 recursively defines the semiring semantics B[[psi]]; Section 3.5 independently defines evaluation trees and proof trees by syntactic decomposition of the formula, with a separate valuation B(T) as product over leaf annotations. Theorem 1 then proves by induction on NNF formulas that B[[psi]] equals the sum of B(T) over all proof trees; this is a genuine combinatorial characterization, not a restatement of the semantics, because the proof-tree notion and its valuation are defined apart from B[[psi]] and the correspondence is established by the induction. Theorem 2 specializes Theorem 1 to model-compatible interpretations, and Corollary 2, Corollary 3, and Proposition 16 are derived consequences rather than assumed inputs. The repair and update results in Sections 6 and 7 are also proved from Theorem 2 and from the specialization construction in Definition 8, not from a fitted parameter or a renamed known result. The finite-universe restriction is stated explicitly and is genuinely essential to the finitary proof-tree sums, but no infinite-universe claim is made. Although the paper cites the authors' prior work [28], [29], and [42] for context and for further developments, the central theorem and its corollaries are proven in line in this manuscript; the load-bearing steps do not reduce to a self-citation chain. No fitted-input-called-prediction step, no uniqueness result imported from the authors' earlier work, and no ansatz smuggled in only via citation appears in the derivation. The paper is therefore not circular.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The central construction is a new algebraic object, but the paper depends on the finiteness of structures and the standard semiring laws. No numeric free parameters are fitted to data; the illustrative examples use arbitrary token and confidence assignments, but these do not affect the theorems.

assumptions (3)
  • domain assumption The universe A is finite and non-empty.
    Quantifier semantics is defined by finite sums and products over A; the paper states that finiteness of the universe is essential (Section 3.1, Definition 2).
  • standard math Semirings are commutative and naturally ordered.
    Definition 1 restricts attention to naturally ordered semirings, excluding rings; all central claims assume this restriction.
  • domain assumption Formula evaluation is compositional from literals using negation normal form, with equality atoms mapped to 0 or 1.
    This is the definitional backbone of the semantics (Definition 2 and Proposition 1), and it fixes the treatment of equality and inequality.
invented entities (1)
  • Dual-indeterminate polynomial semiring N[X,Xbar]
    purpose: Track positive and negative facts simultaneously in provenance analysis of first-order logic with negation.
    Introduced in Section 4.1 as the quotient of a polynomial semiring by the equations x*xbar = 0. Its usefulness is established internally through Theorem 1 and Theorem 2; no external empirical handle is provided.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Provenance Analysis and Semiring Semantics for First-Order Logic." pith.science (2026). https://pith.science/paper/FCENPQDI

@misc{pith2026241207986,
  author       = {Pith},
  title        = {Pith review of: Provenance Analysis and Semiring Semantics for First-Order Logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FCENPQDI}},
  note         = {Machine review of arXiv:2412.07986}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2412.07986 by the authors.

Figure 1
Figure 1. The model We adopt the visual convention of representing the edges of the digraph as solid arrows and of labeling them with positive tokens when we wish to track their presence through model-checking (see , , ) and with 1 when we are not interested in tracking them (not occurring in this example). Moreover, we represent with dashed arrows absent edges, but only those whose absence, however, we also wish to track, by… view at source ↗
Figure 3
Figure 3. The model F 5.1 A Reverse Analysis Example Let = {, , } be a set of ground values. As before, these will eventually play the role of the vertices of a digraph. However, we do not yet specify a set of edges, i.e., we do not specify a finite model with universe. Instead, as illustrated by the dotted edges in [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figure 4
Figure 4. Maximum confidence model with dominant vertex [PITH_FULL_IMAGE:figures/full_fig_p018_4.png] view at source ↗
Figures from the paper (3 more)
Figure 5
Figure 5. Figure 5: The model H What is the corresponding update on the dual polynomial [[]] ? For the provenance polynomials used for positive queries, as in [33], this update is performed by setting = = 0. However, this would result in the polynomial 0. Of course this cannot be right be…
Figure 6
Figure 6. Figure 6: Model M Consider the model and the model-defining provenance-tracking interpretation in [PITH_FULL_IMAGE:figures/full_fig_p020_6.png]
Figure 7
Figure 7. Figure 7: Model C Note that the interpretation illustrated in [PITH_FULL_IMAGE:figures/full_fig_p022_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

44 extracted references · 21 canonical work pages

  1. [28]

    Gr ¨adel and V

    E. Gr ¨adel and V. Tannen. Semiring provenance for first-order mode l checking. arXiv:1712.01980 [cs.LO], 2017. URL: https://arxiv.org/abs/1712.01980, arXiv:1712.01980

    arXiv 2017

  2. [42]

    J. Xu, W. Zhang, A. Alawini, and V. Tannen. Provenance ana lysis for missing answers and integrity repairs. IEEE Data Eng. Bull. , 41(1):39–50, 2018. URL: http://sites.computer.org/debull/A18mar/p39.pdf. 35

    work page 2018

  3. [1]

    K. Amer. Equationally complete classes of commutative mo noids with monus. Alg. Universalis, 18:129–131, 1984

    work page 1984

  4. [2]

    Amsterdamer, S

    Y. Amsterdamer, S. Davidson, D. Deutch, T. Milo, J. Stoyan ovich, and V Tannen. Putting lipstick on pig: Enabling datab ase-style workflow provenance. PVLDB, 5(4):346–357, 2011

    work page 2011

  5. [3]

    On the Limitations of Provenance for Queries With Difference

    Y. Amsterdamer, D. Deutch, and V. Tannen. On the limitatio ns of provenance for queries with difference. In 3rd Workshop on the Theory and Practice of Provenance, TaPP’11, 2011. See also arXiv:1105.2255

    work page Pith review arXiv 2011

  6. [4]

    Provenance for Aggregate Queries

    Y. Amsterdamer, D. Deutch, and V. Tannen. Provenance for a ggregate queries. In Principles of Database Systems, PODS , pages 153–164, 2011. See also arXiv:1101.1110

    work page Pith review arXiv 2011

  7. [5]

    Bertossi

    L. Bertossi. Database repairs and consistent query answe ring: Origins and further developments. In Principles of Database Systems, PODS 2019, pages 48–58. ACM, 2019. doi:10.1145/3294052.3322190

    arXiv 2019

  8. [6]

    Bizi `ere, E

    C. Bizi `ere, E. Gr¨adel, and M. Naaf. Locality theorems in semiring semantics.In Proceedings of MFCS 2023, 2023. Full version: arXiv 2303.12627

    arXiv 2023

Show all 44 references
  1. [7]

    Bogaerts, M

    B. Bogaerts, M. Jakubowski, and J. Van den Bussche. Postul ates for provenance: Instance- based provenance for first-o rder logic. In Companion of the 43rd Symposium on Principles of Database Systems, to appear in PODS 2024. doi:10.1145/3651596

    2024 doi

  2. [8]

    B. Bosbach. Komplement ¨are Halbgruppen. Math. Ann., 161:279–295, 1965

    1965

  3. [9]

    Bourgaux, A

    C. Bourgaux, A. Ozaki, R. Pe ˜naloza, and L. Predoiu. Provenance for the description logic ELHr. In Proceedings of IJCAI 2020, pages 1862–1869, 2020. doi:10.24963/ijcai.2020/258

    2020 doi

  4. [10]

    Brinke, E

    S. Brinke, E. Gr ¨adel, and L. Mrkonji ´c. Ehrenfeucht–Fra ¨ıss´e games in semiring semantics. In Proceedings of CSL 2024, 2024. Full version: arXiv 2308.04910

    2024 arXiv

  5. [11]

    Brinke, E

    S. Brinke, E. Gr ¨adel, L. Mrkonji ´c, and M. Naaf. Semiring provenance in the infinite. In Tannen’s Festschrift, volume 119 of Open Access Series in Informatics, 2024. URL: http://logic.rwth-aachen.de/pub/BrinkeGraedelMrkonjicNaaf24.pdf

    2024

  6. [12]

    Buneman and E

    P. Buneman and E. Clemons. Efficiently monitoring relatio nal databases. ACM Trans. Database Syst. , 4(3):368–382, 1979. doi:10.1145/320083.320099

    1979

  7. [13]

    Dannert and E

    K. Dannert and E. Gr ¨adel. Provenance analysis: A perspective for description l ogics? In C. Lutz et al., editor, Description Logic, Theory Combination, and All That , volume 11560 of Lecture Notes in Computer Science , pages 266–285. Springer, 2019. doi:10.1007/978-3-030-22102-7_12

    2019 doi

  8. [14]

    Dannert and E

    K. Dannert and E. Gr ¨adel. Semiring provenance for guarded logics. In Hajnal Andr ´eka and Istv ´an N ´emeti on Unity of Science: From Computing to Relativity Theory through Algebraic Logi c, Outstanding Contributions to Logic, pages 53–79. Springe r, 2020. doi:10.1007/978-3-...

    2020 doi

  9. [15]

    Dannert, E

    K. Dannert, E. Gr ¨adel, M. Naaf, and V. Tannen. Semiring provenance for fixed-p oint logic. In C. Baier and J. Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), ...

    2021 doi

  10. [16]

    Deutch, T

    D. Deutch, T. Milo, S. Roy, and V. Tannen. Circuits for dat alog provenance. In Proc. 17th International Conference on Database Theory ICDT, pages 201–212. OpenProceedings.org, 2014. doi:10.5441/002/icdt.2014.22

    2014 doi

  11. [17]

    Deutch, Y

    D. Deutch, Y. Moskovitch, and V. Tannen. Provenance-based analysis of data-centric processes. VLDB J., 24(4):583–607, 2015

    2015

  12. [18]

    R. Fagin. Probabilities on finite models. Journal of Symbolic Logic, 41:50–58, 1976. doi:10.1017/S0022481200051756

    1976 doi

  13. [19]

    Foster, T

    J. Foster, T. Green, and V. Tannen. Annotated XML: querie s and provenance. In Proceedings of PODS 2008, pages 271–280, 2008. doi:10.1145/1376916.1376954

    2008

  14. [20]

    Geerts and A

    F. Geerts and A. Poggi. On database query languages for K- relations. Journal of Applied Logic , 8(2):173–185, 2010. doi:10.1016/j.jal.2009.09.001

    2010 doi

  15. [21]

    Geerts, T

    F. Geerts, T. Unger, G. Karvounarakis, I. Fundulaki, and V. Christophides. Algebraic structures for capturing the p rovenance of SPARQL queries. J. ACM, 63(1):7:1–7:63, 2016. doi:10.1145/2810037

    2016 doi

  16. [22]

    B. Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209–441, 2021. doi:10.1561/1900000068

    2021 doi

  17. [23]

    Glebskii, D

    Y. Glebskii, D. Kogan, M. Liogon’kii, and V. Talanov. Range and degree of realizability of formulas in the restrictedpredicate calculus. Kibernetika, 2:17–28, 1969. doi:10.1007/BF01071084

    1969 doi

  18. [24]

    Gr ¨adel, H

    E. Gr ¨adel, H. Helal, M. Naaf, and R. Wilke. Zero-one laws and almos t sure valuations of first-order logic in semiring semantics . In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2...

    2022 arXiv

  19. [25]

    Gr ¨adel, P

    E. Gr ¨adel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Var di, Y. Venema, and S. Weinstein. Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2007. doi:10.1007/3-540-68804-8

    2007 doi

  20. [26]

    Gr ¨adel, N

    E. Gr ¨adel, N. L¨ ucking, and M. Naaf. Semiring provenance for b¨ uc hi games: Strategy analysis with absorptive polynomials. arXiv:2106.12892 [cs.LO], 2021. URL: https://arxiv.org/abs/2106.12892

    2021 arXiv

  21. [27]

    Gr ¨adel and L

    E. Gr ¨adel and L. Mrkonji ´c. Elementary equivalence versus isomorphism in semiring s emantics. In 48th International Collo- quium on Automata, Languages, and Programming (ICALP 2021) , volume 198, pages 133:1–133:20, Dagstuhl, Germany, 2021. doi:10.4230/LIPIcs.ICALP.2021.133

    2021 doi

  22. [29]

    Gr ¨adel and V

    E. Gr ¨adel and V. Tannen. Provenance analysis for logic and games.Moscow Journal of Combinatorics and Number Theory, 9(3):203– 228, 2020. Preprint available at https://arxiv.org/abs/1907.08470. doi:10.2140/moscow.2020.9.203

    2020 arXiv

  23. [30]

    T. Green. Containment of conjunctive queries on annotat ed relations. Theory Comput. Syst. , 49(2):429–459, 2011. doi:10.1007/s00224-011-9327-6

    2011 doi

  24. [31]

    Green, Z

    T. Green, Z. Ives, and V. Tannen. Reconcilable difference s. Theory Comput. Syst. , 49:460–488, 2011. doi:10.1145/1514894.1514920

    2011

  25. [32]

    Green, G

    T. Green, G. Karvounarakis, Z. Ives, and V. Tannen. Updat e exchange with mappings and provenance. In Proceedings of the 33rd International Conference on Very Large Data Bases, University of Vienna, Austria, September 23-27, 2007, pages 675–686, 2007

    2007

  26. [33]

    Green, G

    T. Green, G. Karvounarakis, and V. Tannen. Provenance se mirings. In Principles of Database Systems PODS , pages 31–40. ACM,

  27. [34]

    Herschel and M

    M. Herschel and M. Hern ´andez. Explaining missing answers to SPJUA queries. Proc. VLDB Endow., 3(1):185–196, 2010. URL: http://www.vldb.org/pvldb/vldb2010/pvldb_vol3/R16.pdf, doi:10.14778/1920841.1920869

    2010

  28. [35]

    Herschel, M

    M. Herschel, M. Hern ´andez, and W. Tan. Artemis: A system for analyzing missing an swers. Proc. VLDB Endow., 2(2):1550–1553,

  29. [36]

    Z. Ives, T. Green, G. Karvounarakis, N. Taylor, V. Tannen, P Talukdar, M. Jacob, and F. Pereira. The ORCHESTRA collaborative data sharing system. SIGMOD Record, 37(3):26–32, 2008

    2008

  30. [37]

    Karvounarakis, Z

    G. Karvounarakis, Z. Ives, and V Tannen. Querying data pr ovenance. In Proceedings of the ACM SIGMOD International Conference on Management of Data, SIGMOD 2010, Indianapolis, Indiana, USA, June 6-10, 2010, pages 951–962, 2010

    2010

  31. [38]

    Meliou, W

    A. Meliou, W. Gatterbauer, K. Moore, and D. Suciu. WHY so? or WHY no? functional causality for explaining query answer s. In VLDB workshop on Management of Uncertain Data (MUD 2010) , volume WP10-04 of CTIT Workshop Proceedings Series, pages 3–17, 2010

    2010

  32. [39]

    Moschovakis

    Y. Moschovakis. Elementary induction on abstract structures. North Holland, 1974

    1974

  33. [40]

    M. Naaf. Computing least and greatest fixed points in abso rptive semirings. arXiv:2106.00399 [cs.LO], 2021. URL: https://arxiv.org/abs/2106.00399

    2021 arXiv

  34. [41]

    V. Tannen. Provenance propagation in complex queries. I n In Search of Elegance in the Theory and Practice of Computation - Essays Dedicated to Peter Buneman, pages 483–493, 2013. doi:10.1007/978-3-642-41660-6_26

    2013 doi

  35. [2007]

    doi:10.1145/1265530.1265535

  36. [2009]

    URL: http://www.vldb.org/pvldb/vol2/vldb09-1004.pdf, doi:10.14778/1687553.1687588

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.