Transparent Query Rewriting
SQL queries are automatically rewritten to track provenance circuits – across inner and outer joins, subqueries anywhere (EXISTS, IN, quantified and scalar comparisons), aggregation, set operations, CTEs, and recursive queries (WITH RECURSIVE). No changes to your schema or application code required.
Semiring Provenance
A unified semiring API for Boolean, counting, why-, how-, and which-provenance, symbolic formulas, tropical, Viterbi, Łukasiewicz, and min-max / max-min evaluations – all through one compiled-evaluation path.
Aggregate Provenance
Aggregation results carry provenance too: agg_token values record symbolically how a SUM, COUNT, MIN/MAX, or AVG depends on base tuples, support further arithmetic, evaluate in any m-semiring, and give exact probabilities to HAVING predicates – with SQL-faithful empty-group and NULL semantics.
Probabilistic Databases
Attach probabilities to input tuples and get the probability of every query answer. Ask for a guarantee – exact, or additive / relative (ε, δ) – and a cost-based chooser runs the cheapest method that meets it: independent evaluation, tree decomposition, d-DNNF knowledge compilation, certified-bounds d-trees, sieve, Monte Carlo, Karp-Luby, or weighted model counting. Tractable classes (hierarchical, FD-aware, inversion-free, and Möbius-invertible safe queries) are recognised at the planner and evaluated in polynomial time.
Knowledge Compilation
Compile a Boolean provenance circuit to a CNF and on to a d-DNNF / d-D for exact probability: Tseytin encoding with a variable-to-source-tuple mapping, an in-process tree-decomposition compiler, and a registry of external compilers and weighted model counters (d4, c2d, dsharp, miniC2D, ganak…), with ddnnf_stats to measure the result.
Network Reliability & Reachability
Recursive WITH RECURSIVE reachability becomes exact network reliability: ProvSQL compiles the query along a tree decomposition of the data graph, evaluating a #P-hard problem in time linear in the number of edges on bounded-treewidth graphs – two-terminal and k-terminal reliability, bounded-hop and min-cost paths, on cyclic data too.
Continuous Distributions
First-class random-variable columns. Build queries with twelve continuous families (Normal, Logistic, Gamma, Beta, log-normal, Weibull…), discrete counts, categorical, Gaussian-mixture, and empirical distributions; compare, join, and aggregate them (percentile_cont, corr, stddev, order statistics); evaluate expectations, moments, quantiles, and entropy analytically or by Monte Carlo; condition on filter predicates inline.
Conditioning
Ask conditional questions with one operator: A | B (“A given B”) gives P(A | B), conditional expectations and variances, and truncated distributions – computed exactly and correlation-aware over the shared provenance circuit, uniformly across discrete events, continuous random variables, and probabilistic aggregates.
Latent Variables & Bayesian Inference
A distribution’s own parameters can themselves be random variables, giving compound and hierarchical models. Observing a leaf’s value (X | (Y = c)) then conditions those latent parameters into their Bayesian posterior – in closed form on conjugate pairs, by likelihood weighting otherwise; evidence() reports the marginal likelihood P(data), and shapley_observe() ranks which observation moved the posterior most – all in SQL.
Shapley & Banzhaf Values
Quantify each input tuple’s contribution to a query answer through Shapley and Banzhaf values, computed in a single circuit traversal – and explore them visually in Studio’s Contributions mode: pin a result tuple, get a ranked per-input bar chart.
Where-Provenance
Column-level provenance: track which source cells – not just which rows – each output value was copied or derived from, through projections and equijoins. Studio’s Where mode shows it live: hover an output cell to highlight its origins.
Temporal & Update Provenance
Provenance of data modifications: INSERT / UPDATE / DELETE are tracked as update gates, enabling audit and undo. Combined with the interval-union semiring, validity timestamps turn a provenance-tracked database into a temporal one – time-travel queries included, and explore them visually in Studio’s Temporal mode: as-of, during, and full-history views on an interactive timeline.
ProvSQL Studio
A web UI for provenance inspection, in five modes: render the circuit DAG behind any result token and evaluate any compiled semiring on a pinned subnode, rank inputs by their Shapley contribution, hover output cells to highlight the source rows that produced them, place rows on a validity timeline, or work in notebooks. Available on PyPI as provsql-studio.
Notebooks
Jupyter-style notebooks over a ProvSQL database: SQL, Markdown, circuit, and evaluation cells, per-cell provenance schemes, saved and loaded as standard .ipynb files. The tutorial and the case studies ship as runnable example notebooks.
ProvSQL Playground
The whole system in your browser: PostgreSQL with ProvSQL compiled to WebAssembly, Studio running on top – no install, no server, nothing leaves the page. Pre-loaded databases and runnable notebooks for the tutorial and the case studies.
Case Studies
Eight self-contained worked examples over realistic datasets – from an intelligence agency and an open-science corpus to GTFS-scale transit data, ministers over time, ML wildlife detections, an air-quality sensor network, peer-review assignment, and a pure probability calculator – each pushing a different facet of the system, cross-referenced by a feature coverage matrix. Most run directly in the Playground.
Provenance Export
Get circuits out, in standard formats: human-readable symbolic formulas (sr_formula), W3C-standard PROV-XML interchange (to_provxml), GraphViz-based rendering (view_circuit), and row-per-edge subcircuit introspection (circuit_subgraph) – with leaves labelled from your data through provenance mappings, and every export one click away in Studio’s evaluation strip.
Lean Formalization
The algebraic core – m-semirings, annotated databases, relational-algebra, aggregation and HAVING semantics, query rewriting, circuits, probability and complexity – is formally verified in Lean 4, with machine-checked theorems backing ProvSQL’s architecture.
C/C++ API
Internal C/C++ API for extending ProvSQL with new semirings and gate types.