42 Search Results for "Gottlob, Georg"


Document
First-Order Rewritability of Rule-Based Ontology Mediated Queries with Negation

Authors: Georg Gottlob, Marco Manna, Andreas Pieris, and Aldo Ricioppo

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


Abstract
The idea of using an ontology to enrich user queries with domain knowledge has attracted considerable attention from the database and KR communities during the last fifteen years or so. The ontology and the user query can be conveniently seen as two components of one composite query, called ontology-mediated query (omq), while an omq language (OL,QL) collects all such omqs where the ontology is expressed using the ontology language OL and the user query comes from the query language QL. The evaluation problem for rule-based omq languages of the form (OL,CQ), where OL is a rule-based ontology language, i.e., it collects ontologies modelled using tuple-generating dependencies (a.k.a. existential rules), and CQ is the language of conjunctive queries, has been extensively studied in the literature. In particular, the notion of first-order rewritability of such languages, i.e., the property of being able to rewrite every omq from the language in question to an equivalent first-order query, has been studied in depth. This research effort led an algorithmic characterization of when a rule-based omq language (OL,CQ) is first-order rewritable. More precisely, there is a uniform algorithm Rewrite such that, for every rule-based ontology language OL, the omq language (OL,CQ) is first-order rewritable iff for every omq O from (OL,CQ), the algorithm Rewrite on input O terminates and constructs a first-order rewriting of O. The question that we are interested in is whether the above algorithmic characterization can be extended to rule-based omq languages of the form (OL,nCQ), where nCQ is the language of conjunctive queries with the useful feature of negation. The goal of this work is to initiate effort towards the settlement of the above highly non-trivial question. To this end, we provide a new algorithm, which is a non-trivial extension of the algorithm Rewrite for positive omqs, and show the following: under the Skolem semantics, a well-established approach for defining the answer to a rule-based omq when the user query can use negation, the proposed algorithm is a first-order rewriter for (OL,nCQ), where OL is the language of linear or acyclic tuple-generating dependencies, two central rule-based ontology languages that ensure first-order rewritability for positive omqs. We strongly believe that the new algorithm can serve as a good starting point towards the full settlement of our main question.

Cite as

Georg Gottlob, Marco Manna, Andreas Pieris, and Aldo Ricioppo. First-Order Rewritability of Rule-Based Ontology Mediated Queries with Negation. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{gottlob_et_al:LIPIcs.ICDT.2026.21,
  author =	{Gottlob, Georg and Manna, Marco and Pieris, Andreas and Ricioppo, Aldo},
  title =	{{First-Order Rewritability of Rule-Based Ontology Mediated Queries with Negation}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{21:1--21: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.21},
  URN =		{urn:nbn:de:0030-drops-256353},
  doi =		{10.4230/LIPIcs.ICDT.2026.21},
  annote =	{Keywords: ontology-mediated queries, tuple-generating dependencies, conjunctive queries with negation, first-order rewritability}
}
Document
Random Models and Guarded Logic

Authors: Oskar Fiuk

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


Abstract
Building on ideas of Gurevich and Shelah for the Gödel Class, we present a new probabilistic proof of the finite model property for the Guarded Fragment of First-Order Logic. Our proof is conceptually simple and yields the optimal doubly-exponential upper bound on the size of minimal models. We precisely analyse the obtained bound, up to constant factors in the exponents, and construct sentences that enforce models of tightly matching size. The probabilistic approach adapts naturally to the Triguarded Fragment, an extension of the Guarded Fragment that also subsumes the Two-Variable Fragment. Finally, we derandomise the probabilistic proof by providing an explicit model construction which replaces randomness with deterministic hash functions.

Cite as

Oskar Fiuk. Random Models and Guarded Logic. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{fiuk:LIPIcs.STACS.2026.37,
  author =	{Fiuk, Oskar},
  title =	{{Random Models and Guarded Logic}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{37:1--37:21},
  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.37},
  URN =		{urn:nbn:de:0030-drops-255269},
  doi =		{10.4230/LIPIcs.STACS.2026.37},
  annote =	{Keywords: guarded fragment, finite model property, probabilistic method}
}
Document
Structural Parameterization of Steiner Tree Packing

Authors: Niko Hastrich and Kirill Simonov

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


Abstract
Steiner Tree Packing (STP) is a notoriously hard problem in classical complexity theory, which is of practical relevance to VLSI circuit design. Previous research has approached this problem by providing heuristic or approximate algorithms. In this paper, we show the first FPT algorithms for STP parameterized by structural parameters of the input graph. In particular, we show that STP is fixed-parameter tractable by the tree-cut width as well as the fracture number of the input graph. To achieve our results, we generalize techniques from Edge-Disjoint Paths (EDP) to Generalized Steiner Tree Packing (GSTP), which generalizes both STP and EDP. First, we derive the notion of the augmented graph for GSTP analogous to EDP. We then show that GSTP is FPT by - the tree-cut width of the augmented graph, - the fracture number of the augmented graph, - the slim tree-cut width of the input graph. The latter two results were previously known for EDP; our results generalize these to GSTP and improve the running time for the parameter fracture number. On the other hand, it was open whether EDP is FPT parameterized by the tree-cut width of the augmented graph, despite extensive research on the structural complexity of the problem. We settle this question affirmatively.

Cite as

Niko Hastrich and Kirill Simonov. Structural Parameterization of Steiner Tree Packing. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 51:1-51:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{hastrich_et_al:LIPIcs.STACS.2026.51,
  author =	{Hastrich, Niko and Simonov, Kirill},
  title =	{{Structural Parameterization of Steiner Tree Packing}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{51:1--51: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.51},
  URN =		{urn:nbn:de:0030-drops-255405},
  doi =		{10.4230/LIPIcs.STACS.2026.51},
  annote =	{Keywords: Steiner tree packing, structural parameters, fixed-parameter tractability}
}
Document
Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes

Authors: Manuel Bodirsky and Santiago Guzmán-Pro

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


Abstract
Many computational problems can be modelled as the class of all finite structures A that satisfy a fixed first-order sentence ϕ hereditarily, i.e., we require that every (induced) substructure of A satisfies ϕ. We call the corresponding computational problem the hereditary model checking problem for ϕ, and denote it by Her(ϕ). We present a complete description of the quantifier prefixes for ϕ such that Her(ϕ) is in P; we show that for every other quantifier prefix there exists a formula ϕ with this prefix such that Her(ϕ) is coNP-complete. Specifically, we show that if Q is of the form ∀*∃∀* or of the form ∀*∃*, then Her(ϕ) can be solved in polynomial time whenever the quantifier prefix of ϕ is Q. Otherwise, Q contains ∃∃∀ or ∃∀∃ as a subword, and in this case, there is a first-order formula ϕ whose quantifier prefix is Q and Her(ϕ) is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula ϕ whether Her(ϕ) is in P (unless P=NP).

Cite as

Manuel Bodirsky and Santiago Guzmán-Pro. Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.CSL.2026.6,
  author =	{Bodirsky, Manuel and Guzm\'{a}n-Pro, Santiago},
  title =	{{Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{6:1--6:20},
  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.6},
  URN =		{urn:nbn:de:0030-drops-254308},
  doi =		{10.4230/LIPIcs.CSL.2026.6},
  annote =	{Keywords: Quantifier prefix, first-order Logic, Computational Complexity, Polynomial-time algorithm, coNP-completeness}
}
Document
Invited Paper
ASP Essentials: Modelling and Efficient Solving (Invited Paper)

Authors: Giuseppe Mazzotta and Francesco Ricca

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


Abstract
Answer Set Programming (ASP) is a logic-based Knowledge Representation and Reasoning (KRR) paradigm that facilitates rapid prototyping of solutions for complex problems. It is particularly effective for tackling Deep Reasoning tasks involving exponentially large search spaces, such as combinatorial search and optimization. While getting started with ASP is relatively easy, mastering its advanced constructs and scaling solutions to real-world problem sizes can be challenging. This paper provides an introduction to ASP, guiding the reader from the fundamentals of the language to the application of programming methodologies and the computation of answer sets. Beyond the core framework, the paper also examines selected extensions of ASP that enable the modeling of complex problems, as well as compilation techniques designed to enhance solving efficiency. Furthermore, it mentions some recent tools that combine ASP with LLMs.

Cite as

Giuseppe Mazzotta and Francesco Ricca. ASP Essentials: Modelling and Efficient Solving (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. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{mazzotta_et_al:OASIcs.RW.2024/2025.8,
  author =	{Mazzotta, Giuseppe and Ricca, Francesco},
  title =	{{ASP Essentials: Modelling and Efficient Solving}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{8:1--8:21},
  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.8},
  URN =		{urn:nbn:de:0030-drops-250539},
  doi =		{10.4230/OASIcs.RW.2024/2025.8},
  annote =	{Keywords: Answer Set Programming, ASP with Quantifiers, Grounding Bottleneck, Compilation-based ASP solving, Neurosymbolic AI, LLMs}
}
Document
Invited Paper
Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper)

Authors: Camille Bourgaux

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


Abstract
Real-world datasets are plagued by data quality issues which may render the data inconsistent w.r.t. a set of constraints, be they given by database integrity constraints or ontologies. A prominent way to handle such inconsistent data is to use inconsistency-tolerant semantics to obtain meaningful answers to queries. Most of these semantics are based on some notion of repairs, which represent ways of restoring the data consistency. The most basic kind of repairs is that of subset repairs, which are maximal consistent subsets of the dataset. However, in many scenarios, one can define preferred repairs based on some preference information. These lecture notes present inconsistency-tolerant semantics, focusing on the repair-based ones, then review different kinds of preferred repairs that have been considered in the literature. We present in particular the relationships between different kinds of preferred repairs and other notions related to inconsistency handling, the computational complexity of reasoning with (preferred) repairs, and some implementations.

Cite as

Camille Bourgaux. Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (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. 5:1-5:67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{bourgaux:OASIcs.RW.2024/2025.5,
  author =	{Bourgaux, Camille},
  title =	{{Inconsistency-Tolerant Semantics Based on (Preferred) Repairs}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{5:1--5:67},
  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.5},
  URN =		{urn:nbn:de:0030-drops-250504},
  doi =		{10.4230/OASIcs.RW.2024/2025.5},
  annote =	{Keywords: Knowledge bases, databases, inconsistency handling, repairs, preferences}
}
Document
Invited Paper
Explaining Reasoning Results for Description Logic Ontologies (Invited Paper)

Authors: Patrick Koopmann

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


Abstract
The Web Ontology Language (OWL), grounded in description logics, enables reasoning systems to infer implicit knowledge in a transparent manner. However, the expressivity of description logics and the complexity of large ontologies often results in reasoning outcomes that are hard to understand without additional tool support. Explanations of these outcomes are essential for users to understand ontology content, communicate its structure and behavior effectively, and debug undesired or missing inferences. This chapter provides an overview of the central explanation techniques that have been developed for explaining reasoning with description logic ontologies. Here, we consider both explanations for positive entailments (explaining why something can be deduced), as well as negative entailments (why something cannot be deduced). More specifically, we discuss justifications, proofs and interpolation as a means to explain positive entailments, and abduction for explaining negative entailments, where we also have a closer look at practical algorithms as well as practical and theoretical challenges.

Cite as

Patrick Koopmann. Explaining Reasoning Results for Description Logic Ontologies (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. 6:1-6:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{koopmann:OASIcs.RW.2024/2025.6,
  author =	{Koopmann, Patrick},
  title =	{{Explaining Reasoning Results for Description Logic Ontologies}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{6:1--6:29},
  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.6},
  URN =		{urn:nbn:de:0030-drops-250514},
  doi =		{10.4230/OASIcs.RW.2024/2025.6},
  annote =	{Keywords: Explanations, Justifications, Proofs, Craig Interpolation, Contrastive Explanations}
}
Document
Invited Paper
Fine-Grained Complexity of Ontology Mediated Queries (Invited Paper)

Authors: Cristina Feier

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


Abstract
This article surveys some approaches for establishing fine-grained complexity results for evaluation of ontology mediated queries (OMQs). It accompanies a related talk given at the Reasoning Web Summer School 2024. It zooms into some characterizations of efficiency in a parameterized complexity framework for OMQs based on various description logics and guarded tgds. As such results were established using results from query evaluation on databases, it also discusses the relevant results from the database world. After surveying some successive results on OMQs which all leverage database results in custom ways, it describes an approach which provides a general fpt reduction from query evaluation in the database world to query evaluation in the OMQ world. The reduction enables porting hardness results from the DB world to the OMQ world in a black-box fashion. Along these mentioned approaches, it also provides a brief survey of other approaches which are concerned with fine-grained complexity of OMQs and are based on rewriting techniques.

Cite as

Cristina Feier. Fine-Grained Complexity of Ontology Mediated Queries (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. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{feier:OASIcs.RW.2024/2025.2,
  author =	{Feier, Cristina},
  title =	{{Fine-Grained Complexity of Ontology Mediated Queries}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{2:1--2:23},
  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.2},
  URN =		{urn:nbn:de:0030-drops-250476},
  doi =		{10.4230/OASIcs.RW.2024/2025.2},
  annote =	{Keywords: complexity analysis, guarded logics, guarded tgds, database theory, ontology mediated queries}
}
Document
Invited Paper
Reasoning About Time in DatalogMTL: Course Notes (Invited Paper)

Authors: Przemysław Andrzej Wałęga

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


Abstract
Many real-world applications, such as those in healthcare, finance, and logistics, require reasoning over temporal data. Standard rule-based languages like Datalog, however, lack explicit mechanisms for handling time and temporal dependencies. In this chapter, we discussDatalogMTL, an extension of Datalog with operators frommetric temporal logic that allow to express complex temporal properties. We focus on reasoning algorithms for DatalogMTL, discussing bothmaterialisation, based on fixpoint applications of the immediate consequence operator, and anovel saturation-based extensionthat detects and halts infinite derivations, ensuring both completeness and termination of reasoning.

Cite as

Przemysław Andrzej Wałęga. Reasoning About Time in DatalogMTL: Course Notes (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. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{walega:OASIcs.RW.2024/2025.9,
  author =	{Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  title =	{{Reasoning About Time in DatalogMTL: Course Notes}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{9:1--9:23},
  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.9},
  URN =		{urn:nbn:de:0030-drops-250546},
  doi =		{10.4230/OASIcs.RW.2024/2025.9},
  annote =	{Keywords: DatalogMTL, Logic Programming, Temporal Reasoning}
}
Document
Invited Paper
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
Enumerating the Irreducible Closed Sets of an Acyclic Implicational Base of Bounded Degree

Authors: Oscar Defrain, Arthur Ohana, and Simon Vilmin

Published in: LIPIcs, Volume 359, 36th International Symposium on Algorithms and Computation (ISAAC 2025)


Abstract
We consider the problem of enumerating the irreducible closed sets of a closure system given by an implicational base. To date, the complexity status of this problem is widely open, and it is further known to generalize the notorious hypergraph dualization problem, even in the case of acyclic convex geometries, i.e., closure systems admitting an acyclic implicational base. This paper studies this case with a focus on the degree, which corresponds to the maximal number of implications in which an element occurs. We show that the problem is tractable for bounded values of this parameter, even when relaxed to the notions of premise- and conclusion-degree. Our algorithms rely on a sequential approach leveraging from acyclicity, combined with the solution graph traversal technique for the case of premise-degree. They are shown to perform in incremental-polynomial time. These results are complemented in the long version of this document by showing that the dual problem of constructing the implicational base can be solved in polynomial time. Finally, we argue that our running times cannot be improved to polynomial delay using the standard framework of flashlight search.

Cite as

Oscar Defrain, Arthur Ohana, and Simon Vilmin. Enumerating the Irreducible Closed Sets of an Acyclic Implicational Base of Bounded Degree. In 36th International Symposium on Algorithms and Computation (ISAAC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 359, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{defrain_et_al:LIPIcs.ISAAC.2025.24,
  author =	{Defrain, Oscar and Ohana, Arthur and Vilmin, Simon},
  title =	{{Enumerating the Irreducible Closed Sets of an Acyclic Implicational Base of Bounded Degree}},
  booktitle =	{36th International Symposium on Algorithms and Computation (ISAAC 2025)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-408-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{359},
  editor =	{Chen, Ho-Lin and Hon, Wing-Kai and Tsai, Meng-Tsung},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2025.24},
  URN =		{urn:nbn:de:0030-drops-249321},
  doi =		{10.4230/LIPIcs.ISAAC.2025.24},
  annote =	{Keywords: Algorithmic enumeration, closure systems, acyclic convex geometries, solution graph traversal, flashlight search, extension, hypergraph dualization}
}
Document
Short Paper
The Temporal Vadalog System (Short Paper)

Authors: Luigi Bellomarini, Livia Blasi, Markus Nissl, and Emanuel Sallinger

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)


Abstract
The recent resurgence of the Datalog language in the Knowledge Representation and Reasoning community has paved the way for a very promising proposal for temporal extension. DatalogMTL (Datalog with Metric Temporal Operators) is a language that offers a good trade-off between computational complexity and expressive power. However, existing implementations are still preliminary or prototypical. In this extended abstract, we give a brief overview of Temporal Vadalog, a system supporting reasoning over DatalogMTL programs built upon an engineered architecture and adopted in production scenarios in the financial setting.

Cite as

Luigi Bellomarini, Livia Blasi, Markus Nissl, and Emanuel Sallinger. The Temporal Vadalog System (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 15:1-15:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{bellomarini_et_al:LIPIcs.TIME.2025.15,
  author =	{Bellomarini, Luigi and Blasi, Livia and Nissl, Markus and Sallinger, Emanuel},
  title =	{{The Temporal Vadalog System}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{15:1--15:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.15},
  URN =		{urn:nbn:de:0030-drops-244611},
  doi =		{10.4230/LIPIcs.TIME.2025.15},
  annote =	{Keywords: temporal reasoning, Datalog, DatalogMTL}
}
Document
Semi-Streaming Algorithms for Hypergraph Matching

Authors: Henrik Reinstädtler, S M Ferdous, Alex Pothen, Bora Uçar, and Christian Schulz

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)


Abstract
We propose two one-pass streaming algorithms for the NP-hard hypergraph matching problem. The first algorithm stores a small subset of potential matching edges in a stack using dual variables to select edges. It has an approximation guarantee of 1/(d(1+ε)) and requires 𝒪((n/ε)log²n) bits of memory, where n is the number of vertices in the hypergraph, d is the maximum number of vertices in a hyperedge, and ε > 0 is a parameter to be chosen. The second algorithm computes, stores, and updates a single matching as the edges stream, with an approximation ratio dependent on a parameter α. Its best approximation guarantee is 1/((2d-1) + 2 √{d(d-1)}), and it requires only 𝒪(n) memory. We have implemented both algorithms and compared them with respect to solution quality, memory consumption, and running times on two diverse sets of hypergraphs with a non-streaming greedy and a naive streaming algorithm. Our results show that the streaming algorithms achieve much better solution quality than naive algorithms when facing adverse orderings. Furthermore, these algorithms reduce the memory required by a factor of 13 in the geometric mean on our test problems, and also outperform the offline Greedy algorithm in running time.

Cite as

Henrik Reinstädtler, S M Ferdous, Alex Pothen, Bora Uçar, and Christian Schulz. Semi-Streaming Algorithms for Hypergraph Matching. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 79:1-79:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{reinstadtler_et_al:LIPIcs.ESA.2025.79,
  author =	{Reinst\"{a}dtler, Henrik and Ferdous, S M and Pothen, Alex and U\c{c}ar, Bora and Schulz, Christian},
  title =	{{Semi-Streaming Algorithms for Hypergraph Matching}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{79:1--79:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.79},
  URN =		{urn:nbn:de:0030-drops-245478},
  doi =		{10.4230/LIPIcs.ESA.2025.79},
  annote =	{Keywords: hypergraph, matching, semi-streaming}
}
Document
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
Enumerating Minimal Dominating Sets and Variants in Chordal Bipartite Graphs

Authors: Emanuel Castelo, Oscar Defrain, and Guilherme C. M. Gomes

Published in: LIPIcs, Volume 349, 19th International Symposium on Algorithms and Data Structures (WADS 2025)


Abstract
Enumerating minimal dominating sets with polynomial delay in bipartite graphs is a long-standing open problem. To date, even the subcase of chordal bipartite graphs is open, with the best known algorithm due to Golovach, Heggernes, Kanté, Kratsch, Sæther, and Villanger running in incremental-polynomial time. We improve on this result by providing a polynomial delay and space algorithm enumerating minimal dominating sets in chordal bipartite graphs. Additionally, we show that the total and connected variants admit polynomial and incremental-polynomial delay algorithms, respectively, within the same class. This provides an alternative proof of a result by Golovach et al. for total dominating sets, and answers an open question for the connected variant. Finally, we give evidence that the techniques used in this paper cannot be generalized to bipartite graphs for (total) minimal dominating sets, unless P = NP, and show that enumerating minimal connected dominating sets in bipartite graphs is harder than enumerating minimal transversals in general hypergraphs.

Cite as

Emanuel Castelo, Oscar Defrain, and Guilherme C. M. Gomes. Enumerating Minimal Dominating Sets and Variants in Chordal Bipartite Graphs. In 19th International Symposium on Algorithms and Data Structures (WADS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 349, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{castelo_et_al:LIPIcs.WADS.2025.15,
  author =	{Castelo, Emanuel and Defrain, Oscar and C. M. Gomes, Guilherme},
  title =	{{Enumerating Minimal Dominating Sets and Variants in Chordal Bipartite Graphs}},
  booktitle =	{19th International Symposium on Algorithms and Data Structures (WADS 2025)},
  pages =	{15:1--15:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-398-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{349},
  editor =	{Morin, Pat and Oh, Eunjin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WADS.2025.15},
  URN =		{urn:nbn:de:0030-drops-242467},
  doi =		{10.4230/LIPIcs.WADS.2025.15},
  annote =	{Keywords: algorithmic enumeration, minimal dominating sets, connected dominating sets, total dominating sets, chordal bipartite graphs, sequential method, polynomial delay}
}
  • Refine by Type
  • 42 Document/PDF
  • 33 Document/HTML

  • Refine by Publication Year
  • 4 2026
  • 25 2025
  • 3 2024
  • 4 2023
  • 1 2020
  • Show More...

  • Refine by Author
  • 8 Gottlob, Georg
  • 2 Bellomarini, Luigi
  • 2 Calbimonte, Jean-Paul
  • 2 Defrain, Oscar
  • 2 Dell'Aglio, Daniele
  • Show More...

  • Refine by Series/Journal
  • 28 LIPIcs
  • 7 OASIcs
  • 5 TGDK
  • 1 DagRep
  • 1 DagSemRep

  • Refine by Classification
  • 6 Theory of computation → Logic
  • 5 Computing methodologies → Knowledge representation and reasoning
  • 5 Theory of computation → Constraint and logic programming
  • 4 Mathematics of computing → Enumeration
  • 4 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 4 Datalog
  • 2 DatalogMTL
  • 2 Enumeration
  • 2 Knowledge graphs
  • 2 LLMs
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail