DROPS

Conference

Festschrift Val Tannen (Tannen)

Volume

OASIcs, Volume 119

The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen

Tannen's Festschrift, May 24-25, 2024, University of Pennsylvania, Philadelphia, PA, USA

Editors: Antoine Amarilli and Alin Deutsch

Document

Research

DOI: 10.4230/TGDK.4.1.4

Native Provenance Computation for Federated and Non-Federated SPARQL Queries

Authors: Zubaria Asma, Daniel Hernández, Luis Galárraga, Giorgos Flouris, Irini Fundulaki, and Katja Hose

Published in: TGDK, Volume 4, Issue 1 (2026). Transactions on Graph Data and Knowledge, Volume 4, Issue 1

Abstract

The popularity of knowledge graphs (KGs) owes credit to their flexible data model, which is suitable for data integration from multiple sources. Several KG-based applications, such as trust assessment, view maintenance, or data valuation on dynamic data, rely on the ability to compute provenance explanations for query results. This need becomes more urgent in federated query processing systems, which allow the online consumption of heterogeneous and decentralized Web data. However, the problem of computing and interacting with provenance has received little attention, especially in the federated setting. On those grounds, this paper introduces the NPCS (Native Provenance Computation for SPARQL) approach, and its federated variant Fed-NPCS, that compute provenance for SPARQL query results. Both approaches build upon spm-semirings to annotate the results of monotonic and non-monotonic SPARQL queries with their provenance. Due to their reliance on query rewriting techniques, the approaches are directly applicable to already deployed SPARQL engines and federations using different reification schemes, including RDF-star. Our experimental evaluation shows that our novel query rewriting approach brings significant run-time improvements w.r.t. the state-of-the-art across both centralized and federated settings. In centralized settings, our tests on two popular SPARQL engines (GraphDB and Stardog) reveal substantial runtime gains over existing query rewriting solutions, enabling scalability to RDF graphs with billions of triples. In federated settings, our experiments on the FedShop benchmark with GraphDB show the viability of Fed-NPCS for federations with up to 200 sources.

Cite as

Zubaria Asma, Daniel Hernández, Luis Galárraga, Giorgos Flouris, Irini Fundulaki, and Katja Hose. Native Provenance Computation for Federated and Non-Federated SPARQL Queries. In Transactions on Graph Data and Knowledge (TGDK), Volume 4, Issue 1, pp. 4:1-4:43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{asma_et_al:TGDK.4.1.4,
  author =	{Asma, Zubaria and Hern\'{a}ndez, Daniel and Gal\'{a}rraga, Luis and Flouris, Giorgos and Fundulaki, Irini and Hose, Katja},
  title =	{{Native Provenance Computation for Federated and Non-Federated SPARQL Queries}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:43},
  ISSN =	{2942-7517},
  year =	{2026},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.4.1.4},
  URN =		{urn:nbn:de:0030-drops-259642},
  doi =		{10.4230/TGDK.4.1.4},
  annote =	{Keywords: native provenance computation, federated SPARQL queries, data provenance, NPCS, Fed-NPCS}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2026.12

The Complexity of Finding Missing Answer Repairs

Authors: Jesse Comer and Val Tannen

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)

Abstract

We investigate the problem of identifying database repairs for missing tuples in query answers. We show that when the query is part of the input - the combined complexity setting - determining whether or not a repair exists is polynomial-time equivalent to the satisfiability problem for classes of queries admitting a weak form of projection and selection. We then identify the sub-classes of unions of conjunctive queries with negated atoms, defined by the relational algebra operations permitted to appear in the query, for which the minimal repair problem can be solved in polynomial time. In contrast, we show that the problem is NP-hard, as well as set cover-hard to approximate via strict reductions, whenever both projection and join are permitted in the input query. Additionally, we show that finding the size of a minimal repair for unions of conjunctive queries (with negated atoms permitted) is OptP[log(n)]-complete, while computing a minimal repair is possible with O(n²) queries to an NP oracle. With recursion permitted, the combined complexity of all of these variants increases significantly, with an EXP lower bound. However, from the data complexity perspective, we show that minimal repairs can be identified in polynomial time for all queries expressible as semi-positive datalog programs.

Cite as

Jesse Comer and Val Tannen. The Complexity of Finding Missing Answer Repairs. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{comer_et_al:LIPIcs.ICDT.2026.12,
  author =	{Comer, Jesse and Tannen, Val},
  title =	{{The Complexity of Finding Missing Answer Repairs}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.12},
  URN =		{urn:nbn:de:0030-drops-256265},
  doi =		{10.4230/LIPIcs.ICDT.2026.12},
  annote =	{Keywords: Missing answers, database repairs, datalog, computational complexity}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.STACS.2026.1

Query Languages for Machine-Learning Models (Invited Talk)

Authors: Martin Grohe

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract

In my invited talk and this accompanying paper, I discuss two logics for weighted finite structures: first-order logic with summation (FO(SUM)) and its recursive extension IFP(SUM). These logics originate from foundational work by Grädel, Gurevich, and Meer in the 1990s. In recent joint work with Standke, Steegmans, and Van den Bussche, we have investigated these logics as query languages for machine learning models, specifically neural networks, which are naturally represented as weighted graphs. I present illustrative examples of queries to neural networks that can be expressed in these logics and discuss fundamental results on their expressiveness and computational complexity.

Cite as

Martin Grohe. Query Languages for Machine-Learning Models (Invited Talk). In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{grohe:LIPIcs.STACS.2026.1,
  author =	{Grohe, Martin},
  title =	{{Query Languages for Machine-Learning Models}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{1:1--1:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.1},
  URN =		{urn:nbn:de:0030-drops-254904},
  doi =		{10.4230/LIPIcs.STACS.2026.1},
  annote =	{Keywords: Expressive power of query languages, fixed-point logics, weighted structures, neural networks, explainable AI}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.13

Compactness in Semiring Semantics

Authors: Sophie Brinke, Anuj Dawar, Erich Grädel, Lovro Mrkonjić, and Matthias Naaf

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

Semiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query. To this end, logical statements are not just evaluated to true or false but to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This raises the question to what extent model-theoretic results can be generalised to semiring semantics and how this relates to the algebraic properties of the underlying semiring. Here we investigate the availability of compactness in semiring semantics. The appropriate setting for this is based on absorptive semirings with well-defined infinitary products. Compactness can be stated either in terms of satisfiability or in terms of entailment, and these two variants are trivially equivalent in Boolean semantics. However, this is no longer the case in semiring semantics. Compactness in terms of satisfiability, defined as the existence of non-zero valuations, indeed generalises to every infinitary absorptive semiring. For compactness in terms of entailment the situation is different. The entailment relation naturally extends to semiring semantics (via the natural order on the semiring) but this yields a stronger variant of compactness, which fails for certain important semirings, including the tropical semiring and the Łukasiewicz semiring. Our main positive results show that strong compactness does indeed hold for all finite semirings and all lattice semirings.

Cite as

Sophie Brinke, Anuj Dawar, Erich Grädel, Lovro Mrkonjić, and Matthias Naaf. Compactness in Semiring Semantics. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{brinke_et_al:LIPIcs.CSL.2026.13,
  author =	{Brinke, Sophie and Dawar, Anuj and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro and Naaf, Matthias},
  title =	{{Compactness in Semiring Semantics}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{13:1--13:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.13},
  URN =		{urn:nbn:de:0030-drops-254372},
  doi =		{10.4230/LIPIcs.CSL.2026.13},
  annote =	{Keywords: Semiring semantics, compactness}
}

Document

Invited Paper

DOI: 10.4230/OASIcs.RW.2024/2025.7

Modern Datalog: Concepts, Methods, Applications (Invited Paper)

Authors: Markus Krötzsch

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract

Pure Datalog is arguably the most fundamental rule language, elegant and simple, but also often too limited to be useful in practice. This has motivated the introduction of many new expressive features, ranging from datatypes and related functions, over aggregates and semi-ring generalisations, to existential quantifiers and complex terms. In spite of their variety, all these approaches remain true to the nature of Datalog as a direct, pattern-based way of computing on structured data. We therefore find that a modern notion of Datalog is emerging, distinctly different from other approaches of logic programming and with its own set of related methods and applications. In this course, we introduce Datalog and its most common extensions, and explain when and how these features can be used together (which is often, but not always, safe to do). We further look at modern Datalog systems and some of their primary use cases. Hands-on work with Datalog and its extensions is done with the free Datalog engine https://knowsys.github.io/nemo-doc/. The course is accessible to all audiences and does not assume specific prior knowledge.

Cite as

Markus Krötzsch. Modern Datalog: Concepts, Methods, Applications (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 7:1-7:41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{krotzsch:OASIcs.RW.2024/2025.7,
  author =	{Kr\"{o}tzsch, Markus},
  title =	{{Modern Datalog: Concepts, Methods, Applications}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{7:1--7:41},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.7},
  URN =		{urn:nbn:de:0030-drops-250524},
  doi =		{10.4230/OASIcs.RW.2024/2025.7},
  annote =	{Keywords: Datalog, query language, knowlegde representation and reasoning, logic programming, Horn logic, SPARQL, datatypes and aggregation, lecture notes, tutorial}
}

Document

DOI: 10.4230/LIPIcs.ITP.2025.36

Verifying Datalog Reasoning with Lean

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.

Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tantow_et_al:LIPIcs.ITP.2025.36,
  author =	{Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
  title =	{{Verifying Datalog Reasoning with Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.36},
  URN =		{urn:nbn:de:0030-drops-246342},
  doi =		{10.4230/LIPIcs.ITP.2025.36},
  annote =	{Keywords: Certifying Algorithms, Datalog, Formal Verification}
}

Document

DOI: 10.4230/LIPIcs.ITP.2025.30

Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Authors: Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

We formalize nondeterministic asynchronous dataflow networks in Isabelle/HOL. Dataflow networks are comprised of operators that are capable of communicating with the network, performing silent computations, and making nondeterministic choices. We represent operators using a shallow embedding as codatatypes. Using this representation, we define standard asynchronous dataflow primitives, including sequential and parallel composition and a feedback operator. These primitives adhere to a number of laws from the literature, which we prove by coinduction using weak bisimilarity as our equality. Albeit coinductive and nondeterministic, our model is executable via code extraction to Haskell.

Cite as

Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic Asynchronous Dataflow in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.ITP.2025.30,
  author =	{Silva, Rafael Castro Gon\c{c}alves and Fernet, Laouen and Traytel, Dmitriy},
  title =	{{Nondeterministic Asynchronous Dataflow in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{30:1--30:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.30},
  URN =		{urn:nbn:de:0030-drops-246280},
  doi =		{10.4230/LIPIcs.ITP.2025.30},
  annote =	{Keywords: dataflow, verification, coinduction, Isabelle/HOL}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2025.61

Quantum Relaxations of CSP and Structure Isomorphism

Authors: Amin Karamlou

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract

We investigate quantum relaxations of two key decision problems in computer science: the constraint satisfaction problem (CSP) and the structure isomorphism problem. CSP asks whether a homomorphism exists between two relational structures, while structure isomorphism seeks an isomorphism between them. In recent years, it has become increasingly apparent that many special cases of CSP can be reformulated in terms of the existence of perfect classical strategies in non-local games, a key topic of study in quantum information theory. These games have allowed us to study quantum advantage in relation to many important decision problems, such as the k-colouring problem, and the problem of solving binary constraint systems. Abramsky et al. (2017) have shown that all of these games can be seen as special instances of a non-local CSP game. Moreover, they show that perfect quantum strategies in this CSP game can be viewed as Kleisli morphisms of a graded monad on the category of relational structures, which they dub the quantum monad. In this way, the quantum monad provides a categorical characterisation of quantum advantage for the non-local CSP game. In this work we solidify and expand the results of Abramsky et al., answering several of their open questions. Firstly, we compare the definition of quantum graph homomorphisms arising from this work with an earlier definition of the concept due to Mančinska and Roberson and show that there are graphs which exhibit quantum advantage under one definition but not the other. Our second contribution is to extend the results of Abramsky et al. which only hold in the tensor product framework of quantum mechanics to the commuting operator framework. Next, we study a non-local structure isomorphism game, which generalises the well-studied graph isomorphism game. We show how the construction of the quantum monad can be refined to provide categorical semantics for quantum strategies in this game. This results in a category where morphisms coincide with quantum homomorphisms and isomorphisms coincide with quantum isomorphisms.

Cite as

Amin Karamlou. Quantum Relaxations of CSP and Structure Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 61:1-61:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{karamlou:LIPIcs.MFCS.2025.61,
  author =	{Karamlou, Amin},
  title =	{{Quantum Relaxations of CSP and Structure Isomorphism}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{61:1--61:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.61},
  URN =		{urn:nbn:de:0030-drops-241686},
  doi =		{10.4230/LIPIcs.MFCS.2025.61},
  annote =	{Keywords: CSP, graph isomorphism, quantum information, non-local game, quantum graph homomorphism, monad}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2025.6

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

Authors: Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.

Cite as

Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen. Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2025.6,
  author =	{Ahrens, Emma and Kassing, Jan-Christoph and Giesl, J\"{u}rgen and Katoen, Joost-Pieter},
  title =	{{Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.6},
  URN =		{urn:nbn:de:0030-drops-236215},
  doi =		{10.4230/LIPIcs.FSCD.2025.6},
  annote =	{Keywords: Rewriting, Semirings, Semantics, Termination, Verification}
}

Document

Database Theory in Action

DOI: 10.4230/LIPIcs.ICDT.2025.33

Database Theory in Action: Making Provenance and Probabilistic Database Theory Work in Practice (Invited Talk)

Authors: Silviu Maniu and Pierre Senellart

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

There has been a rich literature in database theory on how to model and manage the provenance of data (for instance using the semiring framework) and its uncertainty (in particular via probabilistic databases). In this article, we explain how these results have been used as the basis for practical implementations, notably in the ProvSQL system, and how these implementations need to be adapted for the efficient management of provenance and probability for real-world data.

Cite as

Silviu Maniu and Pierre Senellart. Database Theory in Action: Making Provenance and Probabilistic Database Theory Work in Practice (Invited Talk). In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 33:1-33:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{maniu_et_al:LIPIcs.ICDT.2025.33,
  author =	{Maniu, Silviu and Senellart, Pierre},
  title =	{{Database Theory in Action: Making Provenance and Probabilistic Database Theory Work in Practice (Invited Talk)}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{33:1--33:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.33},
  URN =		{urn:nbn:de:0030-drops-229746},
  doi =		{10.4230/LIPIcs.ICDT.2025.33},
  annote =	{Keywords: provenance, probabilistic data, ProvSQL}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2025.32

The Free Termination Property of Queries over Time

Authors: Conor Power, Paraschos Koutris, and Joseph M. Hellerstein

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

Building on prior work on distributed databases and the CALM Theorem, we define and study the question of free termination: in the absence of distributed coordination, what query properties allow nodes in a distributed (database) system to unilaterally terminate execution even though they may receive additional data or messages in the future? This completeness question is complementary to the soundness questions studied in the CALM literature. We also develop a new model based on semiautomata that allows us to bridge from the relational transducer model of the CALM papers to algebraic models that are popular among software engineers (e.g. CRDTs) and of increasing interest to database theory for datalog extensions and incremental view maintenance.

Cite as

Conor Power, Paraschos Koutris, and Joseph M. Hellerstein. The Free Termination Property of Queries over Time. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{power_et_al:LIPIcs.ICDT.2025.32,
  author =	{Power, Conor and Koutris, Paraschos and Hellerstein, Joseph M.},
  title =	{{The Free Termination Property of Queries over Time}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.32},
  URN =		{urn:nbn:de:0030-drops-229736},
  doi =		{10.4230/LIPIcs.ICDT.2025.32},
  annote =	{Keywords: distributed systems, algebraic data models, coordination-free systems}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2025.28

Generalized Covers for Conjunctive Queries

Authors: Paraschos Koutris

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

Covers of query results were introduced as succinct lossless representations of join query outputs. A cover is a subset of the query result from which we can efficiently enumerate the output with constant delay and linear preprocessing time. However, covers are dependent on a single tree decomposition of the query. In this work, we generalize the notion of a cover to a set of multiple tree decompositions. We show that this generalization can potentially produce asymptotically smaller covers while maintaining the properties of constant-delay enumeration and linear preprocessing time. In particular, given a set of tree decompositions, we can determine exactly the asymptotic size of a minimum cover, which is tied to the notion of entropic width of the query. We also provide a simple greedy algorithm that computes this cover efficiently. Finally, we relate covers to semiring circuits when the semiring is idempotent.

Cite as

Paraschos Koutris. Generalized Covers for Conjunctive Queries. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koutris:LIPIcs.ICDT.2025.28,
  author =	{Koutris, Paraschos},
  title =	{{Generalized Covers for Conjunctive Queries}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.28},
  URN =		{urn:nbn:de:0030-drops-229698},
  doi =		{10.4230/LIPIcs.ICDT.2025.28},
  annote =	{Keywords: Conjunctive Query, tree decomposition, cover}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2025.12

Tractable Conjunctive Queries over Static and Dynamic Relations

Authors: Ahmet Kara, Zheng Luo, Milos Nikolic, Dan Olteanu, and Haozhe Zhang

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

We investigate the evaluation of conjunctive queries over static and dynamic relations. While static relations are given as input and do not change, dynamic relations are subject to inserts and deletes. We characterise syntactically three classes of queries that admit constant update time and constant enumeration delay. We call such queries tractable. Depending on the class, the preprocessing time is linear, polynomial, or exponential (under data complexity, so the query size is constant). To decide whether a query is tractable, it does not suffice to analyse separately the sub-queries over the static relations and over the dynamic relations, respectively. Instead, we need to take the interaction between the static and the dynamic relations into account. Even when the sub-query over the dynamic relations is not tractable, the overall query can become tractable if the dynamic relations are sufficiently constrained by the static ones.

Cite as

Ahmet Kara, Zheng Luo, Milos Nikolic, Dan Olteanu, and Haozhe Zhang. Tractable Conjunctive Queries over Static and Dynamic Relations. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kara_et_al:LIPIcs.ICDT.2025.12,
  author =	{Kara, Ahmet and Luo, Zheng and Nikolic, Milos and Olteanu, Dan and Zhang, Haozhe},
  title =	{{Tractable Conjunctive Queries over Static and Dynamic Relations}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{12:1--12:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.12},
  URN =		{urn:nbn:de:0030-drops-229534},
  doi =		{10.4230/LIPIcs.ICDT.2025.12},
  annote =	{Keywords: fully dynamic algorithm, constant enumeration delay, constant update time}
}

36 Search Results for "Tannen, Val"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message