Pith. sign in

REVIEW 3 cited by

Semiring Provenance for First-Order Model Checking

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1712.01980 v1 pith:3547PGWC submitted 2017-12-06 cs.LO

Erich Grädel , Val Tannen This is my paper · ORCID
classification cs.LO
keywords provenancefirst-ordergivenpolynomialscommutativecomputationdatamodel
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Codd's Theorem for Databases over Semirings

    cs.LO 2025-01 conditional novelty 8.0 of 10

    Codd's theorem, the equivalence of relational algebra and relational calculus, is extended to semiring-annotated databases, with a proof that division is not expressible from the five basic operations over bag databases.

  2. Rewriting Consistent Answers on Annotated Data

    cs.DB 2024-12 conditional novelty 7.0 of 10

    Consistent answers of self-join-free conjunctive queries over naturally ordered positive semirings are rewritable in the logic LK exactly when the query's attack graph is acyclic, generalizing the Boolean case.

  3. Provenance Analysis and Semiring Semantics for First-Order Logic

    cs.LO 2024-12 accept novelty 5.0 of 10

    Dual-indeterminate polynomial semirings provide a provenance semantics for full first-order logic with negation, enabling reverse provenance analysis and repair computation.

Pith tools