26 citations · 29 across the 7 of their papers we have counts for
5 papers · 1 filter
Provenance Analysis and Semiring Semantics for First-Order Logic
Erich Grädel, Val Tannen
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. Traditiona…
Syntax Monads for the Working Formal Metatheorist
Lawrence Dunn, Val Tannen, Steve Zdancewic
Formally verifying the properties of formal systems using a proof assistant requires justifying numerous minor lemmas about capture-avoiding substitution. Despite work on category-…
Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic
Katrin M. Dannert, Erich Grädel, Matthias Naaf +1
Semiring provenance is a successful approach to provide detailed information on the combinations of atomic facts that are responsible for the result of a query. In particular, inte…
Provenance Analysis for Logic and Games
Erich Grädel, Val Tannen
A model checking computation checks whether a given logical sentence is true in a given finite structure. Provenance analysis abstracts from such a computation mathematical informa…
Semiring Provenance for First-Order Model Checking
Erich Grädel, Val Tannen
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 abst…