International Center for Computational Logic - Benutzerbeiträge [de]

Inproceedings3464

2026-04-17T06:58:17Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Lukas |ErsterAutorNachname=Gerlach }} {{Inproceedings |Referiert=1 |Title=The Chase in Lean - Crafting a Formal Library for Existential Rule Research |To appear=1 |Year=2026 |Booktitle=KR 2026 }} {{Publikation Details |Abstract=The chase is a sound, complete, but possibly non-terminating algorithm for reasoning with existential rules (aka. tuple-generating dependencies), a highly expressive knowledge represen…“

{{Publikation Erster Autor
|ErsterAutorVorname=Lukas
|ErsterAutorNachname=Gerlach
}}
{{Inproceedings
|Referiert=1
|Title=The Chase in Lean - Crafting a Formal Library for Existential Rule Research
|To appear=1
|Year=2026
|Booktitle=KR 2026
}}
{{Publikation Details
|Abstract=The chase is a sound, complete, but possibly non-terminating algorithm for reasoning with existential rules (aka. tuple-generating dependencies), a highly expressive knowledge representation language. Although the procedure appears simple, research on theoretical properties and optimization for practical implementations has grown to a point where verifying correctness and reproducing proofs becomes challenging and intuition can sometimes be misleading. Lean is a purely functional programming language and interactive theorem prover whose community actively develops formal libraries for mathematics (Mathlib) and computer science (CSLib). In this work, we present our own endeavor of crafting a Lean framework around existential rules and the chase. We discuss design decisions concerning the nuances of chase definitions commonly found in the literature and show how these translate into Lean. To illustrate the framework’s capabilities using known results, we show that the result of a chase is a universal model and outline the formalization for proving that without so-called “alternative matches” it is even a core. Beyond existing literature, we unify sufficient chase termination conditions in the likeness of Model-Faithful Acyclicity (MFA) into a common framework while also adding support for constants in rules.
|Download=KR-2026-Camera-Ready-178-Chase-In-Lean.pdf
|Link=https://dmfa.dev/lean
|Projekt=CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}

Datei:KR-2026-Camera-Ready-178-Chase-In-Lean.pdf

2026-04-17T06:57:12Z

Lukas Gerlach:

Inproceedings3430

2026-04-17T06:54:24Z

Lukas Gerlach:

{{Publikation Erster Autor
|ErsterAutorVorname=David
|ErsterAutorNachname=Carral
|FurtherAuthors=Lukas Gerlach; Lucas Larroque; Michaël Thomazo
}}
{{Inproceedings
|Referiert=1
|Title=Restricted Chase Termination: You Want More than Fairness (Extended Abstract)
|To appear=0
|Year=2025
|Month=September
|Booktitle=Proceedings of the 38th International Workshop on Description Logics - DL 2025
|Publisher=CEUR-WS.org
|Editor=Lidia Tendera,Yazmin Ibanez Garcia,Patrick Koopmann
|Series=CEUR Workshop Proceedings
|Volume=4091
}}
{{Publikation Details
|Abstract=The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for many chase variants, which differ by the conditions under which a rule is applied to extend the database. Surprisingly, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition, and we propose an alternative to reduce the hardness of universal termination.
|ISSN=1613-0073
|Download=DL-2025-Camera-Ready-5.pdf
|Slides=2025-DL-Presentation-Paper-5.pdf
|Link=https://ceur-ws.org/Vol-4091/paper05.pdf
|Projekt=CPEC, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}

Lukas Gerlach

2026-03-04T07:20:56Z

Lukas Gerlach:

{{Mitarbeiter
|Vorname=Lukas
|Nachname=Gerlach
|Akademischer Titel=Dipl.-Inf.
|Forschungsgruppe=Wissensbasierte Systeme
|Stellung=Wissenschaftlicher Mitarbeiter
|Ehemaliger=0
|Telefon=+49 351 463 43503
|Email=lukas.gerlach@tu-dresden.de
|Matrix=@s8339654:tu-dresden.de
|Raum=APB 3031
|Bild=Lukas-Gerlach-Profile-Picture.jpg
|Info='''Hi!'''

Ich bin Lukas und wissenschaftlicher Mitarbeiter / Doktorand in der Forschungsgruppe [[Wissensbasierte Systeme]].
Ich forsche hauptsächlich an [[Existenzielle Regeln|Existenziellen Regeln]], dem Chase Algorithmus und verwandten Themen.
In meinem Studium habe ich mich vertiefend mit Datenbanktheorie, Logik und Komplexitätstheorie beschäftigt.
Außerdem habe ich eine Leidenschaft für [https://lean-lang.org/ Lean].
|Info EN='''Hi!'''

I'm Lukas and I'm a Research Associate / PhD student in the [[Knowledge-Based Systems]] group.
I mainly research [[Existenzielle Regeln/en|existential rules]], the chase algorithm and related topics.
During my studies, I specialized in database theory, logics and complexity theory.
Also, I have a passion for [https://lean-lang.org/ Lean].
|DBLP=https://dblp.org/pid/156/3555-2.html
|Google Scholar=https://scholar.google.com/citations?user=IIoVutAAAAAJ
|Alternative URI=https://monsterkrampe.dev/
|Public Key=Public-key-lukas-gerlach.asc
|Publikationen anzeigen=1
|Abschlussarbeiten anzeigen=1
|Projekte anzeigen=0
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}

Lukas Gerlach

2026-03-04T07:20:36Z

Lukas Gerlach:

{{Mitarbeiter
|Vorname=Lukas
|Nachname=Gerlach
|Akademischer Titel=Dipl.-Inf.
|Forschungsgruppe=Wissensbasierte Systeme
|Stellung=Wissenschaftlicher Mitarbeiter
|Ehemaliger=0
|Telefon=+49 351 463 43503
|Email=lukas.gerlach@tu-dresden.de
|Matrix=@s8339654:tu-dresden.de
|Raum=APB 3031
|Bild=Me.jpg Lukas-Gerlach-Profile-Picture.jpg
|Info='''Hi!'''

Ich bin Lukas und wissenschaftlicher Mitarbeiter / Doktorand in der Forschungsgruppe [[Wissensbasierte Systeme]].
Ich forsche hauptsächlich an [[Existenzielle Regeln|Existenziellen Regeln]], dem Chase Algorithmus und verwandten Themen.
In meinem Studium habe ich mich vertiefend mit Datenbanktheorie, Logik und Komplexitätstheorie beschäftigt.
Außerdem habe ich eine Leidenschaft für [https://lean-lang.org/ Lean].
|Info EN='''Hi!'''

I'm Lukas and I'm a Research Associate / PhD student in the [[Knowledge-Based Systems]] group.
I mainly research [[Existenzielle Regeln/en|existential rules]], the chase algorithm and related topics.
During my studies, I specialized in database theory, logics and complexity theory.
Also, I have a passion for [https://lean-lang.org/ Lean].
|DBLP=https://dblp.org/pid/156/3555-2.html
|Google Scholar=https://scholar.google.com/citations?user=IIoVutAAAAAJ
|Alternative URI=https://monsterkrampe.dev/
|Public Key=Public-key-lukas-gerlach.asc
|Publikationen anzeigen=1
|Abschlussarbeiten anzeigen=1
|Projekte anzeigen=0
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}

Datei:Lukas-Gerlach-Profile-Picture.jpg

2026-03-04T07:20:31Z

Lukas Gerlach:

Research Seminar Logic and AI

2026-02-12T06:49:43Z

Lukas Gerlach:

{{#leftsidenav:{{LeftsidenavHeading|Contents}}
<div class="no-toc-head">__TOC__</div>
|{{Main heading|Research Seminar on Logic and AI}}

In this research seminar, we invite speakers to present their research on (inter-disciplinary) topics related to logic and artificial intelligence. This includes presentations of published or accepted papers, rehearsals for future talks at conferences, defenses of very good student theses, as well as presentations of ongoing research. All are welcome!

The seminar is organized by the [[Computational Logic/en|Computational Logic]] group. Please contact [[Meghna Bhadra/en|Meghna Bhadra]], if you would like to give a talk or invite a guest speaker.

===Schedule and Location===

The research seminar is scheduled on Thursdays from 11.00 am to 12.00 pm. It is held in a hybrid form, both online through [https://bbb.tu-dresden.de/rooms/sqo-ezi-97u-sry/join Big Blue Button] and physically in the room APB-2026.
For further information on an upcoming seminar pease check the program overview for the same.

====Recent and Upcoming Talks====

<table class="table" >
<tr><th>Date</th><th>Speaker</th><th>Topic</th></tr>
{{#ask: [[Event series::Research Seminar Logic and AI]]
| ?Titel EN=
| ?Datum#ISO=
| ?Vortragender=
| sort=Datum
| order=desc
| format=plainlist
| template=Talk short inline/en
| searchlabel=
| link=none
| limit=5
}}
<tr><td></td><td>{{#ask: [[Event series::Research Seminar Logic and AI]]|
| ?Datum=Date
| ?=Title
| ?Vortragender=Speaker
| mainlabel=-
| sort=Datum | order=desc | limit=0 | searchlabel=View older talks …}}</td><td>{{Upcoming events feed
| L=/en
| query=[[Event series::Research Seminar Logic and AI]]
| label=Subscribe to upcoming talks (iCal)
| calendartitle=ICCL Research Seminar Logic and AI
}}</td></tr>
</table>

===Calendar===

{{#ask:[[Event series::Research Seminar Logic and AI]][[Start::+]]
| ?Start
| ?Ende
| ?Titel EN=title
| ?Raum=Room
| ?Veranstaltungsart=<br/>Type
| ?Vortragender=<br/>Speaker
| ?Beschreibung EN=<br/>Details
| format=eventcalendar
| firstday=Monday
| defaultview=month
| limit=1000
| link=subject
}}

}}

{{#set:
|Title=Research Seminar Logic and AI
|Forschungsgruppe=Computational Logic
|Lecturer=Sebastian Rudolph
|Lecturer=Thomas Feller
|Modul=INF-AQUA
|Modul=INF-PM-FOR
|Term=WS
|Year=2020
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
}}
{{#subobject:
|Title=Research Seminar Logic and AI
|Forschungsgruppe=Computational Logic
|Lecturer=Sebastian Rudolph
|Lecturer=Thomas Feller
|Modul=INF-AQUA
|Modul=INF-PM-FOR
|Term=SS
|Year=2021
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|@category=Vorlesung
}}
{{#subobject:
|Title=Research Seminar Logic and AI
|Forschungsgruppe=Wissensbasierte Systeme
|Lecturer=Markus Krötzsch
|Lecturer=Ali Elhalawati
|Modul=INF-AQUA
|Modul=INF-PM-FOR
|Term=WS
|Year=2021
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|@category=Vorlesung
}}
{{#subobject:
|Title=Research Seminar Logic and AI
|Forschungsgruppe=Wissensbasierte Systeme
|Lecturer=Markus Krötzsch
|Lecturer=Ali Elhalawati
|Modul=INF-AQUA
|Modul=INF-PM-FOR
|Term=SS
|Year=2022
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|@category=Vorlesung
}}
{{#subobject:
|Title=Research Seminar Logic and AI
|Forschungsgruppe=Computational Logic
|Lecturer=Sebastian Rudolph
|Lecturer=Piotr Ostropolski-Nalewaja
|Modul=INF-AQUA
|Modul=INF-PM-FOR
|Term=WS
|Year=2022
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|@category=Vorlesung
}}
{{#subobject:
|Title=Research Seminar Logic and AI
|Forschungsgruppe=Computational Logic
|Lecturer=Sebastian Rudolph
|Lecturer=Piotr Ostropolski-Nalewaja
|Modul=INF-AQUA
|Modul=INF-PM-FOR
|Term=SS
|Year=2023
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|@category=Vorlesung
}}
{{#subobject:
|Title=Research Seminar Logic and AI
|Forschungsgruppe=Computational Logic
|Lecturer=Sebastian Rudolph
|Lecturer=Piotr Ostropolski-Nalewaja
|Modul=INF-AQUA
|Modul=INF-PM-FOR
|Term=WS
|Year=2023
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|@category=Vorlesung
}}

[[Kategorie:Event series]] [[Kategorie:Vorlesung]]

Inproceedings3429

2025-11-24T09:10:48Z

Lukas Gerlach:

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean (Extended Abstract)
|To appear=0
|Year=2025
|Month=November
|Booktitle=KR 2025 - Recently Published Research Track
}}
{{Publikation Details
|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, 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 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.
|Download=KR-2025-Camera-Ready-389.pdf
|Slides=KR-2025-Verifying-Datalog-Reasoning-with-Lean-Slides.pdf
|Link=https://kr.org/KR2025/files/rpr-papers/389%20-%20Verifying%20Datalog%20Reasoning%20with%20Lean.pdf
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

Datei:KR-2025-Verifying-Datalog-Reasoning-with-Lean-Slides.pdf

2025-11-24T09:10:30Z

Lukas Gerlach:

Inproceedings3434

2025-11-24T09:07:08Z

Lukas Gerlach:

{{Publikation Erster Autor
|ErsterAutorVorname=Lukas
|ErsterAutorNachname=Gerlach
|FurtherAuthors=Lucas Larroque; Jerzy Marcinkowski; Piotr Ostropolski-Nalewaja
}}
{{Inproceedings
|Referiert=1
|Title=About the Multi-Head Linear Restricted Chase Termination
|To appear=0
|Year=2025
|Month=Oktober
|Booktitle=Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025)
|Pages=346-355
|Publisher=IJCAI Organization
|Editor=Magdalena Ortiz,Renata Wassermann,Torsten Schaub
|Series=Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning
|Volume=22
}}
{{Publikation Details
|Abstract=The chase is a ubiquitous algorithm in database theory. However, for existential rules (aka tuple-generating dependencies), its termination is not guaranteed, and even undecidable in general. The problem of termination becomes particularly difficult for the restricted (or standard) chase, for which the order of rule application matters. Thus, decidability of restricted chase termination is still open for many well-behaved classes such as linear or guarded multi-headed rules. We make a step forward by showing that all-instances restricted chase termination is decidable in the linear multi-headed case.
|ISBN=978-1-956792-08-9
|ISSN=2334-1033
|Download=KR-2025-Linear-Multi-Head-Termination.pdf
|Slides=KR-2025-About-the-Multi-Head-Linear-Restricted-Chase-Termination-Slides.pdf
|DOI Name=10.24963/kr.2025/34
|Projekt=Cfaed, CPEC, CeTI, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}

Datei:KR-2025-About-the-Multi-Head-Linear-Restricted-Chase-Termination-Slides.pdf

2025-11-24T09:07:01Z

Lukas Gerlach:

Inproceedings3417

2025-09-25T05:37:15Z

Lukas Gerlach:

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean
|To appear=0
|Year=2025
|Month=September
|Booktitle=16th International Conference on Interactive Theorem Proving (ITP 2025)
|Pages=36:1-36:19
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik
|Editor=Yannick Forster, Chantal Keller
|Series=Leibniz International Proceedings in Informatics (LIPIcs)
|Volume=352
}}
{{Publikation Tool
|Tool=Nemo
}}
{{Publikation Details
|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.
|Download=ITP-2025-Paper-116-Camera-Ready.pdf
|Link=https://github.com/knowsys/CertifyingDatalog
|DOI Name=10.4230/LIPIcs.ITP.2025.36
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

Inproceedings3434

2025-09-23T06:16:37Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Lukas |ErsterAutorNachname=Gerlach |FurtherAuthors=Lucas Larroque; Jerzy Marcinkowski; Piotr Ostropolski-Nalewaja }} {{Inproceedings |Referiert=1 |Title=About the Multi-Head Linear Restricted Chase Termination |To appear=1 |Year=2025 |Month=November |Booktitle=KR 2025 }} {{Publikation Details |Abstract=The chase is a ubiquitous algorithm in database theory. However, for existential rules (aka tuple-generating…“

{{Publikation Erster Autor
|ErsterAutorVorname=Lukas
|ErsterAutorNachname=Gerlach
|FurtherAuthors=Lucas Larroque; Jerzy Marcinkowski; Piotr Ostropolski-Nalewaja
}}
{{Inproceedings
|Referiert=1
|Title=About the Multi-Head Linear Restricted Chase Termination
|To appear=1
|Year=2025
|Month=November
|Booktitle=KR 2025
}}
{{Publikation Details
|Abstract=The chase is a ubiquitous algorithm in database theory. However, for existential rules (aka tuple-generating dependencies), its termination is not guaranteed, and even undecidable in general. The problem of termination becomes particularly difficult for the restricted (or standard) chase, for which the order of rule application matters. Thus, decidability of restricted chase termination is still open for many well-behaved classes such as linear or guarded multi-headed rules. We make a step forward by showing that all-instances restricted chase termination is decidable in the linear multi-headed case.
|Download=KR-2025-Linear-Multi-Head-Termination.pdf
|Projekt=Cfaed, CPEC, CeTI, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}

Datei:KR-2025-Linear-Multi-Head-Termination.pdf

2025-09-23T06:15:15Z

Lukas Gerlach:

Supporting Risk Management for Medical Devices via the Riskman Ontology and Shapes

2025-09-23T05:19:39Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Supporting Risk Management for Medical Devices via the Riskman Ontology and Shapes |Beschreibung EN=We propose the Riskman ontology and shapes for representing and analysing information about risk management for medical devices. Risk management is concerned with taking necessary precautions to ensure that a medical device does not cause harms for users or the environment. To date, risk management documentation is submitted to not…“

{{Veranstaltung
|Titel EN=Supporting Risk Management for Medical Devices via the Riskman Ontology and Shapes
|Beschreibung EN=We propose the Riskman ontology and shapes for representing and analysing information about risk management for medical devices. Risk management is concerned with taking necessary precautions to ensure that a medical device does not cause harms for users or the environment. To date, risk management documentation is submitted to notified bodies (for certification) in the form of semi-structured natural language text. We propose to use terms from the Riskman ontology to provide a formal, logical underpinning for risk management documentation, and to use the included SHACL constraints to check whether the provided data is in accordance with the requirements of the two relevant norms, i.e. ISO 14971 and VDE Spec 90025.
|Veranstaltungsart=Vortrag
|Start=2025-09-25 11:00:00
|Ende=2025-09-25 12:00:00
|Raum=APB 3027
|Vortragender=Piotr Gorczyca
|URL=https://iccl.inf.tu-dresden.de/web/Inproceedings3424/en
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Reliance-based Static Analysis of Existential Rules

2025-09-16T04:42:50Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Reliance-based Static Analysis of Existential Rules |Beschreibung EN=Cores are universal models of existential rules knowledge bases that have no redundant facts. They can be determined with the core chase, but this is expensive. Recent work suggested special positive and restraint reliance relations between rules to assess whether applying a rule can activate another and whether a rule should be preferred over another to avoid i…“

{{Veranstaltung
|Titel EN=Reliance-based Static Analysis of Existential Rules
|Beschreibung EN=Cores are universal models of existential rules knowledge bases that have no redundant facts. They can be determined with the core chase, but this is expensive. Recent work suggested special positive and restraint reliance relations between rules to assess whether applying a rule can activate another and whether a rule should be preferred over another to avoid introducing unnecessary facts into the chase result. They give rise to core-stratifiable rulesets, which are susceptible to a rule-based selection strategy for the restricted chase that does not violate restraints and thus produces a core with certainty. However, there are still many practically relevant rulesets which are not core-stratifiable whilst still supporting core computation with a specialized selection strategy for the restricted chase.

We examine such cases to propose a new class of rulesets, which we call SCC-contraction core-stratifiable, that broadens the applicability of the restricted chase to compute cores. It is based on deputizing positive reliances by sets of contracted rules, which are formed by syntactically intersecting unifiable parts of the second rule’s body and the first rule’s head to attain the combined effect of applying two respective triggers in succession. Then, rulesets are contraction core-stratifiable iff they have no cycle in the restraints of the contracted reliance graph. We evaluate a prototype implementation on a subset of the Oxford Ontology Repository, revealing that a significant portion is covered by our analysis.
|Veranstaltungsart=Verteidigung Studienarbeit
|Start=2025-09-18 08:00:00
|Ende=2025-09-18 09:00:00
|Raum=APB 3027
|Vortragender=Nils Küchenmeister
|Forschungsgruppe=Wissensbasierte Systeme
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Software Verification in Ada/SPARK

2025-09-09T11:11:50Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Software Verification in Ada/SPARK |Beschreibung EN=Formal software verification seeks to establish logical properties of programs with mathematical rigor, rather than relying solely on empirical testing. Ada/SPARK provides a verification-oriented programming environment in which contracts (preconditions, postconditions, invariants) serve as logical specifications embedded in the code. These contracts enable modular reasoning abo…“

{{Veranstaltung
|Titel EN=Software Verification in Ada/SPARK
|Beschreibung EN=Formal software verification seeks to establish logical properties of programs with mathematical rigor, rather than relying solely on empirical testing. Ada/SPARK provides a verification-oriented programming environment in which contracts (preconditions, postconditions, invariants) serve as logical specifications embedded in the code. These contracts enable modular reasoning about subprograms and allow the GNATprove tool to discharge proofs of safety properties, functional correctness and termination. I will outline this verification
workflow, illustrate typical classes of provable properties and discuss current industrial applications.
|Veranstaltungsart=Vortrag
|Start=2025-10-16 11:00:00
|Ende=2025-10-16 12:00:00
|Raum=APB 3027
|Vortragender=Marcos Cramer
|Forschungsgruppe=Wissensbasierte Systeme
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Linear Ghost Types Are All You Need -- An Introduction to Proof-Oriented Programming in Verus

2025-09-09T05:12:54Z

Lukas Gerlach:

{{Veranstaltung
|Titel EN=Linear Ghost Types Are All You Need - An Introduction to Proof-Oriented Programming in Verus
|Beschreibung EN=Previously in this seminar, we introduced a concurrent separation logic (IRIS) to verify the memory safety of unsafe code inside Rust's standard library. Conversely, the observation that the safe subset of Rust can be efficiently encoded into constraint horn clauses has led to highly automated, SMT-solver based tools for the verification of this subset of rust. Naturally, the next question is how to automate the verification of Rust programs that do use unsafe code. Linear ghost types offer a simple yet powerful solution: We can reuse the borrow checking that is already performed by the Rust compiler to automate a separation logic built into the source code, allowing for a "proof oriented programming" style. In this talk, we show how linear ghost types relate to the broader landscape of verification tools for Rust and how to use them for the verification of low level data structures -- an application which might be useful for nemo, the Rust-based logic reasoner developed in our group.
|Veranstaltungsart=Verteidigung Studienarbeit
|Start=2025-09-11 11:00:00
|Ende=2025-09-11 12:00:00
|Raum=APB 3027
|Vortragender=Matthias Meißner
|Forschungsgruppe=Wissensbasierte Systeme
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Linear Ghost Types Are All You Need -- An Introduction to Proof-Oriented Programming in Verus

2025-09-09T05:10:59Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Linear Ghost Types Are All You Need -- An Introduction to Proof-Oriented Programming in Verus |Beschreibung EN=Previously in this seminar, we introduced a concurrent separation logic (IRIS) to verify the memory safety of unsafe code inside Rust's standard library. Conversely, the observation that the safe subset of Rust can be efficiently encoded into constraint horn clauses has led to highly automated, SMT-solver based tools for…“

{{Veranstaltung
|Titel EN=Linear Ghost Types Are All You Need -- An Introduction to Proof-Oriented Programming in Verus
|Beschreibung EN=Previously in this seminar, we introduced a concurrent separation logic (IRIS) to verify the memory safety of unsafe code inside Rust's standard library. Conversely, the observation that the safe subset of Rust can be efficiently encoded into constraint horn clauses has led to highly automated, SMT-solver based tools for the verification of this subset of rust. Naturally, the next question is how to automate the verification of Rust programs that do use unsafe code. Linear ghost types offer a simple yet powerful solution: We can reuse the borrow checking that is already performed by the Rust compiler to automate a separation logic built into the source code, allowing for a "proof oriented programming" style. In this talk, we show how linear ghost types relate to the broader landscape of verification tools for Rust and how to use them for the verification of low level data structures -- an application which might be useful for nemo, the Rust-based logic reasoner developed in our group.
|Veranstaltungsart=Verteidigung Studienarbeit
|Start=2025-09-11 11:00:00
|Ende=2025-09-11 12:00:00
|Raum=APB 3027
|Vortragender=Matthias Meißner
|Forschungsgruppe=Wissensbasierte Systeme
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Inproceedings3430

2025-09-01T06:52:18Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=David |ErsterAutorNachname=Carral |FurtherAuthors=Lukas Gerlach; Lucas Larroque; Michaël Thomazo }} {{Inproceedings |Referiert=1 |Title=Restricted Chase Termination: You Want More than Fairness (Extended Abstract) |To appear=1 |Year=2025 |Month=September |Booktitle=DL Workshop 2025 }} {{Publikation Details |Abstract=The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a databas…“

{{Publikation Erster Autor
|ErsterAutorVorname=David
|ErsterAutorNachname=Carral
|FurtherAuthors=Lukas Gerlach; Lucas Larroque; Michaël Thomazo
}}
{{Inproceedings
|Referiert=1
|Title=Restricted Chase Termination: You Want More than Fairness (Extended Abstract)
|To appear=1
|Year=2025
|Month=September
|Booktitle=DL Workshop 2025
}}
{{Publikation Details
|Abstract=The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in a most general way. This process may not terminate, and a major problem is to decide whether it does. This problem has been studied for many chase variants, which differ by the conditions under which a rule is applied to extend the database. Surprisingly, the complexity of the universal termination of the restricted (aka standard) chase is not fully understood. We close this gap by placing universal restricted chase termination in the analytical hierarchy. This higher hardness is due to the fairness condition, and we propose an alternative to reduce the hardness of universal termination.
|Download=DL-2025-Camera-Ready-5.pdf
|Slides=2025-DL-Presentation-Paper-5.pdf
|Projekt=CPEC, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}

Datei:2025-DL-Presentation-Paper-5.pdf

2025-09-01T06:52:13Z

Lukas Gerlach:

Datei:DL-2025-Camera-Ready-5.pdf

2025-09-01T06:43:31Z

Lukas Gerlach:

Inproceedings3429

2025-09-01T06:38:27Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Johannes |ErsterAutorNachname=Tantow |FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch }} {{Inproceedings |Referiert=1 |Title=Verifying Datalog Reasoning with Lean (Extended Abstract) |To appear=1 |Year=2025 |Month=November |Booktitle=KR 2025 - Recently Published Research Track }} {{Publikation Details |Abstract=Datalog is an essential logical rule language with many applications and modern ru…“

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean (Extended Abstract)
|To appear=1
|Year=2025
|Month=November
|Booktitle=KR 2025 - Recently Published Research Track
}}
{{Publikation Details
|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, 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 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.
|Download=KR-2025-Camera-Ready-389.pdf
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

Datei:KR-2025-Camera-Ready-389.pdf

2025-09-01T06:37:05Z

Lukas Gerlach:

A Crash Course in Determinacy

2025-08-20T05:57:43Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=A Crash Course in Determinacy |Beschreibung EN=This talk offers a (short) crash course in Determinacy - a classical problem in database theory, and with multiple connections to KR. At its core, the determinacy problem asks: given a query Q and a set of queries {V_1, V_2, ..., V_n}, can the answer to Q(D) be recovered solely from the answers to V_1(D), V_2(D), ..., V_n(D) no matter the database D? We will explore the p…“

{{Veranstaltung
|Titel EN=A Crash Course in Determinacy
|Beschreibung EN=This talk offers a (short) crash course in Determinacy - a classical problem in database theory, and with multiple connections to KR.

At its core, the determinacy problem asks: given a query Q and a set of queries {V_1, V_2, ..., V_n}, can the answer to Q(D) be recovered solely from the answers to V_1(D), V_2(D), ..., V_n(D) no matter the database D?

We will explore the problem, its key variants, and the connections to query rewritability, existential rules, and the chase procedure. The presentation will be grounded in examples, making the concepts as concrete and intuitive as possible.

The presentation will be given on the board, so do feel encouraged to join the talk in person if possible. We will provide the usual hybrid setup but it will likely be hard to see what is written on the board online. Sorry for the inconvenience!
|Veranstaltungsart=Vortrag
|Start=2025-08-21 11:00:00
|Ende=2025-08-21 12:00:00
|Raum=APB 3027
|Vortragender=Piotr Ostropolski-Nalewaja
|Eingeladen durch=Sebastian Rudolph
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

LogAI-Seminar-2025-06-19

2025-07-28T12:59:29Z

Lukas Gerlach:

{{Veranstaltung
|Titel EN=Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics
|Beschreibung EN=Fuzzy logic programming is an established approach for reasoning under uncertainty.
Several semantics from classical, two-valued logic programming have been generalized to the case of fuzzy logic programs.
In this paper, we show that two of the most prominent classical semantics, namely the stable model and the well-founded semantics, can be reconstructed within the general framework of approximation fixpoint theory (AFT).

This not only widens the scope of AFT from two- to many-valued logics, but allows a wide range of existing AFT results to be applied to fuzzy logic programming.
As first examples of such applications, we clarify the formal relationship between existing semantics, generalize the notion of stratification from classical to fuzzy logic programs, and devise “more precise” variants of the semantics.
|Veranstaltungsart=Vortrag
|Start=2025-07-31 11:00:00
|Ende=2025-07-31 12:00:00
|Raum=APB 3027
|Vortragender=Pascal Kettmann
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

LogAI-Seminar-2025-08-14

2025-07-25T08:56:13Z

Lukas Gerlach:

{{Veranstaltung
|Titel EN=PhD Status Talk: Multi-agent Belief Management
|Beschreibung EN=In epistemic voting, multiple agents vote over a set of alternatives, with the goal of identifying the one that corresponds to the ground truth. The Condorcet Jury Theorem (CJT) is a foundational result in this context, offering probabilistic guarantees for truth-tracking, albeit under restrictive assumptions. This talk has two main objectives. First, we generalize the CJT by relaxing its core assumptions and provide novel probabilistic bounds for successful truth identification. Second, we introduce a new aggregation method, Voting for Bins, grounded in the epistemic voting framework, designed for aggregating interval-valued probabilistic beliefs. Each of these contributions is tied to a key application: for the generalized CJT, we formalize and bound conditions under which diversity can outperform ability, offering a rigorous formulation of the Diversity-Trumps-Ability Theorem. For Voting for Bins, we address the problem of dilation in imprecise belief aggregation.
|Veranstaltungsart=Vortrag
|Start=2025-08-14 11:00:00
|Ende=2025-08-14 12:00:00
|Raum=APB 3027
|Vortragender=Jonas Karge
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Satisfying Rationality Postulates of Structured Argumentation through Deductive Support

2025-07-21T14:19:23Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Satisfying Rationality Postulates of Structured Argumentation through Deductive Support |Beschreibung EN=ASPIC-style structured argumentation frameworks provide a formal basis for reasoning in artificial intelligence by combining internal argument structure with abstract argumentation semantics. A key challenge in these frameworks is ensuring compliance with five critical rationality postulates: closure, direct consistency, indir…“

{{Veranstaltung
|Titel EN=Satisfying Rationality Postulates of Structured Argumentation through Deductive Support
|Beschreibung EN=ASPIC-style structured argumentation frameworks provide a formal basis for reasoning in artificial intelligence by combining internal argument structure with abstract argumentation semantics. A key challenge in these frameworks is ensuring compliance with five critical rationality postulates: closure, direct consistency, indirect consistency, non-interference, and crash-resistance. Recent approaches, including ASPIC⊖ and Deductive ASPIC-, have made significant progress but fall short of meeting all postulates simultaneously under a credulous semantics (e.g. preferred) in the presence of undercuts. We introduce Deductive ASPIC⊖, a novel framework that integrates gen-rebuttals from ASPIC⊖ with the Joint Support Bipolar Argumentation Frameworks (JSBAFs) of Deductive ASPIC-, incorporating preferences. We show that Deductive ASPIC⊖ satisfies all five rationality postulates under a version of preferred semantics.
|Veranstaltungsart=Vortrag
|Start=2025-07-24 11:00:00
|Ende=2025-07-24 12:00:00
|Raum=APB 3027
|Vortragender=Tom Friese
|Forschungsgruppe=Wissensbasierte Systeme
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

LogAI-Seminar-2025-06-19

2025-07-21T14:18:08Z

Lukas Gerlach:

{{Veranstaltung
|Titel EN=Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics
|Beschreibung EN=Fuzzy logic programming is an established approach for reasoning under uncertainty.
Several semantics from classical, two-valued logic programming have been generalized to the case of fuzzy logic programs.
In this paper, we show that two of the most prominent classical semantics, namely the stable model and the well-founded semantics, can be reconstructed within the general framework of approximation fixpoint theory (AFT).

This not only widens the scope of AFT from two- to many-valued logics, but allows a wide range of existing AFT results to be applied to fuzzy logic programming.
As first examples of such applications, we clarify the formal relationship between existing semantics, generalize the notion of stratification from classical to fuzzy logic programs, and devise “more precise” variants of the semantics.
|Veranstaltungsart=Vortrag
|Start=2025-08-07 11:00:00
|Ende=2025-08-07 12:00:00
|Raum=APB 3027
|Vortragender=Pascal Kettmann
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Datei:ITP-2025-Paper-116-Camera-Ready.pdf

2025-07-16T06:31:57Z

Lukas Gerlach: Lukas Gerlach lud eine neue Version von Datei:ITP-2025-Paper-116-Camera-Ready.pdf hoch

Inproceedings3417

2025-07-14T07:35:07Z

Lukas Gerlach:

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean
|To appear=1
|Year=2025
|Month=September
|Booktitle=16th International Conference on Interactive Theorem Proving (ITP 2025)
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik
|Editor=Yannick Forster, Chantal Keller
|Series=LIPIcs
|Volume=352
}}
{{Publikation Details
|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.
|Download=ITP-2025-Paper-116-Camera-Ready.pdf
|Link=https://github.com/knowsys/CertifyingDatalog
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

Inproceedings3417

2025-07-14T07:21:05Z

Lukas Gerlach:

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean
|To appear=1
|Year=2025
|Month=September
|Booktitle=16th International Conference on Interactive Theorem Proving (ITP 2025)
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik}
|Editor=Yannick Forster, Chantal Keller
|Series=LIPIcs
|Volume=352
}}
{{Publikation Details
|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.
|Download=ITP-2025-Paper-116-Camera-Ready.pdf
|Link=https://github.com/knowsys/CertifyingDatalog
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

Inproceedings3417

2025-07-14T07:20:17Z

Lukas Gerlach: Änderung 42595 von Lukas Gerlach (Diskussion) rückgängig gemacht.

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean
|To appear=1
|Year=2025
|Month=September
|Booktitle=ITP 2025
}}
{{Publikation Details
|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.
|Download=ITP-2025-Paper-116-Camera-Ready.pdf
|Link=https://github.com/knowsys/CertifyingDatalog
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

Inproceedings3417

2025-07-14T07:19:02Z

Lukas Gerlach:

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean
|To appear=1
|Year=2025
|Month=September
|Booktitle=16th Conference on Interactive Theorem Proving (ITP 2025)
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik
|Editor=Yannick Forster, Chantal Keller
|Series=LIPIcs
|Volume=352
}}
{{Publikation Details
|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.
|Download=ITP-2025-Paper-116-Camera-Ready.pdf
|Link=https://github.com/knowsys/CertifyingDatalog
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

LogAI-Seminar-2025-06-19

2025-07-10T05:01:55Z

Lukas Gerlach:

{{Veranstaltung
|Titel EN=POSTPONED - Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics
|Beschreibung EN=Fuzzy logic programming is an established approach for reasoning under uncertainty.
Several semantics from classical, two-valued logic programming have been generalized to the case of fuzzy logic programs.
In this paper, we show that two of the most prominent classical semantics, namely the stable model and the well-founded semantics, can be reconstructed within the general framework of approximation fixpoint theory (AFT).

This not only widens the scope of AFT from two- to many-valued logics, but allows a wide range of existing AFT results to be applied to fuzzy logic programming.
As first examples of such applications, we clarify the formal relationship between existing semantics, generalize the notion of stratification from classical to fuzzy logic programs, and devise “more precise” variants of the semantics.
|Veranstaltungsart=Vortrag
|Start=2025-07-10 11:00:00
|Ende=2025-07-10 12:00:00
|Raum=APB 3027
|Vortragender=Pascal Kettmann
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Database Theory (SS2025)

2025-07-09T05:53:03Z

Lukas Gerlach:

{{Vorlesung
|Title=Database Theory
|Research group=Wissensbasierte Systeme
|Lecturers=Markus Krötzsch
|Tutors=Lukas Gerlach
|Term=SS
|Year=2025
|Lecture series=Database Theory
|Matrix=#dbt2025:tu-dresden.de
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-PM-FOR, INF-VERT6, MCL-KR, MCL-PI, MCL-TCSL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=mündliche Prüfung
|Description=Databases are a key technology in computer science that brings together fascinating theoretical topics and highly relevant practical applications. The goal of this lecture is to give an extended introduction to this interesting field, with a special focus on database query languages, their expressive power, and computational complexity. The lecture will introduce the relational data model, and then discuss theoretical and practical aspects of a variety of query languages:

* first-order logic as a query language and the relational algebra
* conjunctive queries and their unions
* navigational queries: path queries
* Datalog and its relatives
* query answering under database dependencies

The lecture focuses on core principles that apply to many types of databases alike (relational, graph-based, semantic web). Some important query answering algorithms are presented, too, but otherwise, the details of database implementation and administration are not covered.

===Prerequisites===

Undergraduate-level knowledge of predicate logic, regular languages, and algorithmic and computational complexity is required. The lecture will connect with other topics in the Computer Science and Computational Logic curriculum, such as relational databases, logic programming, and Semantic Web technologies – familiarity with these topics is not required to follow the lecture.

===Schedule and Location===

* The weekly lecture sessions will take place on Mondays from 09:20 to 10:50 in room [[APB E007]] and Tuesdays from 09:20 to 10:50 in room [[APB E005]].
* The weekly exercise session will take place on Tuesdays from 14:50 to 16:20 in room [[APB E005]].
* The first exercise session will be on Tuesday, 2025-04-15.

===Examinations===
Dates for oral exams will be announced in due time.
As usual, you should book a date with our [mailto:secretary_wbs@mailbox.tu-dresden.de secretary] after you have officially enrolled in your respective examination office/system.

===Legacy===

This course has first been taught at TU Dresden by Prof. Dr. [[Markus Krötzsch]] in the form of the 2015 lecture [[Foundations_of_Databases_and_Query_Languages_(SS2015)/en|Foundations of Databases and Query Languages]], and later in the [[Database_Theory/en|Database Theory]] lecture series. The plan for this year's course will be somewhat similar.

The structure of some of the lectures of this course is inspired by the course ''Theory of Data and Knowledge Bases'' in the version given by [https://www.cs.ox.ac.uk/people/georg.gottlob/ Georg Gottlob] and [http://www.cs.ox.ac.uk/people/thomas.lukasiewicz/ Thomas Lukasiewicz] at the University of Oxford.
|Literature=The main reference textbook for the lecture is:
* Serge Abiteboul, Richard Hull, Victor Vianu: Foundations of Databases. Addison-Wesley. 1994.
: ''The book is available for free from [http://webdam.inria.fr/Alice/ its webpage], but there are also copies in the library.''

Further texts might be consulted for background information and additional details:
* Michael Sipser: Introduction to the Theory of Computation. 2005
: ''Accessible introduction to complexity theory that covers all topics of computational complexity that the lecture touches upon.''
* Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov: Complexity and expressive power of logic programming. ACM Computing Surveys, 33:3, pp 374-425, 2001.
: ''Covers all Datalog complexity results mentioned in the lecture. Available at http://dx.doi.org/10.1145/502807.502810 (may require access from within a university network)''
* ''additional references may be added in the course of the lecture''
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction/Relational Data Model
|Room=APB E007
|Date=2025-04-07
|DS=DS2
|Download=DBT2025-Lecture-01-overlay.pdf, DBT2025-Lecture-01-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=First-Order Queries
|Room=APB E005
|Date=2025-04-08
|DS=DS2
|Download=DBT2025-Lecture-02-overlay.pdf, DBT2025-Lecture-02-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Complexity of Query Answering
|Room=APB E007
|Date=2025-04-14
|DS=DS2
|Download=DBT2025-Lecture-03-overlay.pdf, DBT2025-Lecture-03-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Complexity of FO Query Answering
|Room=APB E005
|Date=2025-04-15
|DS=DS2
|Download=DBT2025-Lecture-04-overlay.pdf, DBT2025-Lecture-04-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=1. Relational Algebra
|Room=APB E005
|Date=2025-04-15
|DS=DS5
|Download=DBT-2025-Exercise-01.pdf, DBT-2025-Exercise-01-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Easter Monday
|Room=APB E007
|Date=2025-04-21
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Data Complexity of FO Query Answering
|Room=APB E005
|Date=2025-04-22
|DS=DS2
|Download=DBT2025-Lecture-05-overlay.pdf, DBT2025-Lecture-05-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=2. First-Order Queries
|Room=APB E005
|Date=2025-04-22
|DS=DS5
|Download=DBT-2025-Exercise-02.pdf, DBT-2025-Exercise-02-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Conjunctive Queries
|Room=APB E007
|Date=2025-04-28
|DS=DS2
|Download=DBT2025-Lecture-06-overlay.pdf, DBT2025-Lecture-06-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Tree-Like Conjunctive Queries (1)
|Room=APB E005
|Date=2025-04-29
|DS=DS2
|Download=DBT2025-Lecture-07-overlay.pdf, DBT2025-Lecture-07-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=3. Complexity of First-Order Queries
|Room=APB E005
|Date=2025-04-29
|DS=DS5
|Download=DBT-2025-Exercise-03.pdf, DBT-2025-Exercise-03-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Tree-Like Conjunctive Queries (2)
|Room=APB E007
|Date=2025-05-05
|DS=DS2
|Download=DBT2025-Lecture-08-overlay.pdf, DBT2025-Lecture-08-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Optimisation
|Room=APB E005
|Date=2025-05-06
|DS=DS2
|Download=DBT2025-Lecture-09-overlay.pdf, DBT2025-Lecture-09-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=4. Conjunctive Queries, CSP, and Hypergraphs
|Room=APB E005
|Date=2025-05-06
|DS=DS5
|Download=DBT-2025-Exercise-04.pdf, DBT-2025-Exercise-04-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Conjunctive Query Optimisation
|Room=APB E007
|Date=2025-05-12
|DS=DS2
|Download=DBT2025-Lecture-10-overlay.pdf, DBT2025-Lecture-10-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness
|Room=APB E005
|Date=2025-05-13
|DS=DS2
|Download=DBT2025-Lecture-11-overlay.pdf, DBT2025-Lecture-11-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=5. Tree Width and Hypertree Width
|Room=APB E005
|Date=2025-05-13
|DS=DS5
|Download=DBT-2025-Exercise-05.pdf, DBT-2025-Exercise-05-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness (continued)
|Room=APB E007
|Date=2025-05-19
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness (continued)
|Room=APB E005
|Date=2025-05-20
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=6. Trakhtenbrot's Theorem
|Room=APB E005
|Date=2025-05-20
|DS=DS5
|Download=DBT-2025-Exercise-06.pdf, DBT-2025-Exercise-06-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction to Datalog / Datalog Complexity
|Room=APB E007
|Date=2025-05-26
|DS=DS2
|Download=DBT2025-Lecture-12-overlay.pdf, DBT2025-Lecture-12-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction to Datalog / Datalog Complexity (continued)
|Room=APB E005
|Date=2025-05-27
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=7. FO Query Expressivity
|Room=APB E005
|Date=2025-05-27
|DS=DS5
|Download=DBT-2025-Exercise-07.pdf, DBT-2025-Exercise-07-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Expressivity and Containment
|Room=APB E007
|Date=2025-06-02
|DS=DS2
|Download=DBT2025-Lecture-13-overlay.pdf, DBT2025-Lecture-13-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Expressivity and Containment (continued)
|Room=APB E005
|Date=2025-06-03
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=8. Datalog
|Room=APB E005
|Date=2025-06-03
|DS=DS5
|Download=DBT-2025-Exercise-08.pdf, DBT-2025-Exercise-08-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Pentecost
|Room=APB E007
|Date=2025-06-09
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Pentecost
|Room=APB E005
|Date=2025-06-10
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Exercise: Pentecost
|Room=APB E005
|Date=2025-06-10
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Evaluation (1)
|Room=APB E007
|Date=2025-06-16
|DS=DS2
|Download=DBT2025-Lecture-14-overlay.pdf, DBT2025-Lecture-14-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Evaluation (2) / Graph Databases
|Room=APB E005
|Date=2025-06-17
|DS=DS2
|Download=DBT2025-Lecture-15-overlay.pdf, DBT2025-Lecture-15-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=9. Semi-Positive Datalog
|Room=APB E005
|Date=2025-06-17
|DS=DS5
|Download=DBT-2025-Exercise-09.pdf, DBT-2025-Exercise-09-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Path Queries
|Room=APB E007
|Date=2025-06-23
|DS=DS2
|Download=DBT2025-Lecture-16-overlay.pdf, DBT2025-Lecture-16-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Dependencies
|Room=APB E005
|Date=2025-06-24
|DS=DS2
|Download=DBT2025-Lecture-17-overlay.pdf, DBT2025-Lecture-17-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=10. Datalog Evaluation
|Room=APB E005
|Date=2025-06-24
|DS=DS5
|Download=DBT-2025-Exercise-10.pdf, DBT-2025-Exercise-10-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The Chase
|Room=APB E007
|Date=2025-06-30
|DS=DS2
|Download=DBT2025-Lecture-18-overlay.pdf, DBT2025-Lecture-18-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No lecture
|Room=APB E005
|Date=2025-07-01
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=11. Graph Databases and Path Queries
|Room=APB E005
|Date=2025-07-01
|DS=DS5
|Download=DBT-2025-Exercise-11.pdf, DBT-2025-Exercise-11-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The Chase (continued; termination and acyclicity)
|Room=APB E007
|Date=2025-07-07
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Answering Beyond Acyclic TGDs
|Room=APB E005
|Date=2025-07-08
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=12. Dependencies
|Room=APB E005
|Date=2025-07-08
|DS=DS5
|Download=DBT-2025-Exercise-12.pdf, DBT-2025-Exercise-12-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Outlook/Summary
|Room=APB E007
|Date=2025-07-14
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Konsultation
|Title=Consultation (time for your questions)
|Room=APB E005
|Date=2025-07-15
|DS=DS2
}}

Datei:DBT-2025-Exercise-12-Slides.pdf

2025-07-09T05:52:56Z

Lukas Gerlach:

LogAI-Seminar-2025-06-19

2025-07-08T08:06:22Z

Lukas Gerlach:

{{Veranstaltung
|Titel EN=Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics
|Beschreibung EN=Fuzzy logic programming is an established approach for reasoning under uncertainty.
Several semantics from classical, two-valued logic programming have been generalized to the case of fuzzy logic programs.
In this paper, we show that two of the most prominent classical semantics, namely the stable model and the well-founded semantics, can be reconstructed within the general framework of approximation fixpoint theory (AFT).

This not only widens the scope of AFT from two- to many-valued logics, but allows a wide range of existing AFT results to be applied to fuzzy logic programming.
As first examples of such applications, we clarify the formal relationship between existing semantics, generalize the notion of stratification from classical to fuzzy logic programs, and devise “more precise” variants of the semantics.
|Veranstaltungsart=Vortrag
|Start=2025-07-10 11:00:00
|Ende=2025-07-10 12:00:00
|Raum=APB 3027
|Vortragender=Pascal Kettmann
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Database Theory (SS2025)

2025-07-01T14:50:23Z

Lukas Gerlach:

{{Vorlesung
|Title=Database Theory
|Research group=Wissensbasierte Systeme
|Lecturers=Markus Krötzsch
|Tutors=Lukas Gerlach
|Term=SS
|Year=2025
|Lecture series=Database Theory
|Matrix=#dbt2025:tu-dresden.de
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-PM-FOR, INF-VERT6, MCL-KR, MCL-PI, MCL-TCSL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=mündliche Prüfung
|Description=Databases are a key technology in computer science that brings together fascinating theoretical topics and highly relevant practical applications. The goal of this lecture is to give an extended introduction to this interesting field, with a special focus on database query languages, their expressive power, and computational complexity. The lecture will introduce the relational data model, and then discuss theoretical and practical aspects of a variety of query languages:

* first-order logic as a query language and the relational algebra
* conjunctive queries and their unions
* navigational queries: path queries
* Datalog and its relatives
* query answering under database dependencies

The lecture focuses on core principles that apply to many types of databases alike (relational, graph-based, semantic web). Some important query answering algorithms are presented, too, but otherwise, the details of database implementation and administration are not covered.

===Prerequisites===

Undergraduate-level knowledge of predicate logic, regular languages, and algorithmic and computational complexity is required. The lecture will connect with other topics in the Computer Science and Computational Logic curriculum, such as relational databases, logic programming, and Semantic Web technologies – familiarity with these topics is not required to follow the lecture.

===Schedule and Location===

* The weekly lecture sessions will take place on Mondays from 09:20 to 10:50 in room [[APB E007]] and Tuesdays from 09:20 to 10:50 in room [[APB E005]].
* The weekly exercise session will take place on Tuesdays from 14:50 to 16:20 in room [[APB E005]].
* The first exercise session will be on Tuesday, 2025-04-15.

===Examinations===
Dates for oral exams will be announced in due time.
As usual, you should book a date with our [mailto:secretary_wbs@mailbox.tu-dresden.de secretary] after you have officially enrolled in your respective examination office/system.

===Legacy===

This course has first been taught at TU Dresden by Prof. Dr. [[Markus Krötzsch]] in the form of the 2015 lecture [[Foundations_of_Databases_and_Query_Languages_(SS2015)/en|Foundations of Databases and Query Languages]], and later in the [[Database_Theory/en|Database Theory]] lecture series. The plan for this year's course will be somewhat similar.

The structure of some of the lectures of this course is inspired by the course ''Theory of Data and Knowledge Bases'' in the version given by [https://www.cs.ox.ac.uk/people/georg.gottlob/ Georg Gottlob] and [http://www.cs.ox.ac.uk/people/thomas.lukasiewicz/ Thomas Lukasiewicz] at the University of Oxford.
|Literature=The main reference textbook for the lecture is:
* Serge Abiteboul, Richard Hull, Victor Vianu: Foundations of Databases. Addison-Wesley. 1994.
: ''The book is available for free from [http://webdam.inria.fr/Alice/ its webpage], but there are also copies in the library.''

Further texts might be consulted for background information and additional details:
* Michael Sipser: Introduction to the Theory of Computation. 2005
: ''Accessible introduction to complexity theory that covers all topics of computational complexity that the lecture touches upon.''
* Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov: Complexity and expressive power of logic programming. ACM Computing Surveys, 33:3, pp 374-425, 2001.
: ''Covers all Datalog complexity results mentioned in the lecture. Available at http://dx.doi.org/10.1145/502807.502810 (may require access from within a university network)''
* ''additional references may be added in the course of the lecture''
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction/Relational Data Model
|Room=APB E007
|Date=2025-04-07
|DS=DS2
|Download=DBT2025-Lecture-01-overlay.pdf, DBT2025-Lecture-01-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=First-Order Queries
|Room=APB E005
|Date=2025-04-08
|DS=DS2
|Download=DBT2025-Lecture-02-overlay.pdf, DBT2025-Lecture-02-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Complexity of Query Answering
|Room=APB E007
|Date=2025-04-14
|DS=DS2
|Download=DBT2025-Lecture-03-overlay.pdf, DBT2025-Lecture-03-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Complexity of FO Query Answering
|Room=APB E005
|Date=2025-04-15
|DS=DS2
|Download=DBT2025-Lecture-04-overlay.pdf, DBT2025-Lecture-04-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=1. Relational Algebra
|Room=APB E005
|Date=2025-04-15
|DS=DS5
|Download=DBT-2025-Exercise-01.pdf, DBT-2025-Exercise-01-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Easter Monday
|Room=APB E007
|Date=2025-04-21
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Data Complexity of FO Query Answering
|Room=APB E005
|Date=2025-04-22
|DS=DS2
|Download=DBT2025-Lecture-05-overlay.pdf, DBT2025-Lecture-05-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=2. First-Order Queries
|Room=APB E005
|Date=2025-04-22
|DS=DS5
|Download=DBT-2025-Exercise-02.pdf, DBT-2025-Exercise-02-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Conjunctive Queries
|Room=APB E007
|Date=2025-04-28
|DS=DS2
|Download=DBT2025-Lecture-06-overlay.pdf, DBT2025-Lecture-06-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Tree-Like Conjunctive Queries (1)
|Room=APB E005
|Date=2025-04-29
|DS=DS2
|Download=DBT2025-Lecture-07-overlay.pdf, DBT2025-Lecture-07-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=3. Complexity of First-Order Queries
|Room=APB E005
|Date=2025-04-29
|DS=DS5
|Download=DBT-2025-Exercise-03.pdf, DBT-2025-Exercise-03-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Tree-Like Conjunctive Queries (2)
|Room=APB E007
|Date=2025-05-05
|DS=DS2
|Download=DBT2025-Lecture-08-overlay.pdf, DBT2025-Lecture-08-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Optimisation
|Room=APB E005
|Date=2025-05-06
|DS=DS2
|Download=DBT2025-Lecture-09-overlay.pdf, DBT2025-Lecture-09-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=4. Conjunctive Queries, CSP, and Hypergraphs
|Room=APB E005
|Date=2025-05-06
|DS=DS5
|Download=DBT-2025-Exercise-04.pdf, DBT-2025-Exercise-04-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Conjunctive Query Optimisation
|Room=APB E007
|Date=2025-05-12
|DS=DS2
|Download=DBT2025-Lecture-10-overlay.pdf, DBT2025-Lecture-10-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness
|Room=APB E005
|Date=2025-05-13
|DS=DS2
|Download=DBT2025-Lecture-11-overlay.pdf, DBT2025-Lecture-11-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=5. Tree Width and Hypertree Width
|Room=APB E005
|Date=2025-05-13
|DS=DS5
|Download=DBT-2025-Exercise-05.pdf, DBT-2025-Exercise-05-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness (continued)
|Room=APB E007
|Date=2025-05-19
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness (continued)
|Room=APB E005
|Date=2025-05-20
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=6. Trakhtenbrot's Theorem
|Room=APB E005
|Date=2025-05-20
|DS=DS5
|Download=DBT-2025-Exercise-06.pdf, DBT-2025-Exercise-06-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction to Datalog / Datalog Complexity
|Room=APB E007
|Date=2025-05-26
|DS=DS2
|Download=DBT2025-Lecture-12-overlay.pdf, DBT2025-Lecture-12-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction to Datalog / Datalog Complexity (continued)
|Room=APB E005
|Date=2025-05-27
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=7. FO Query Expressivity
|Room=APB E005
|Date=2025-05-27
|DS=DS5
|Download=DBT-2025-Exercise-07.pdf, DBT-2025-Exercise-07-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Expressivity and Containment
|Room=APB E007
|Date=2025-06-02
|DS=DS2
|Download=DBT2025-Lecture-13-overlay.pdf, DBT2025-Lecture-13-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Expressivity and Containment (continued)
|Room=APB E005
|Date=2025-06-03
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=8. Datalog
|Room=APB E005
|Date=2025-06-03
|DS=DS5
|Download=DBT-2025-Exercise-08.pdf, DBT-2025-Exercise-08-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Pentecost
|Room=APB E007
|Date=2025-06-09
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Pentecost
|Room=APB E005
|Date=2025-06-10
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Exercise: Pentecost
|Room=APB E005
|Date=2025-06-10
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Evaluation (1)
|Room=APB E007
|Date=2025-06-16
|DS=DS2
|Download=DBT2025-Lecture-14-overlay.pdf, DBT2025-Lecture-14-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Evaluation (2) / Graph Databases
|Room=APB E005
|Date=2025-06-17
|DS=DS2
|Download=DBT2025-Lecture-15-overlay.pdf, DBT2025-Lecture-15-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=9. Semi-Positive Datalog
|Room=APB E005
|Date=2025-06-17
|DS=DS5
|Download=DBT-2025-Exercise-09.pdf, DBT-2025-Exercise-09-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Path Queries
|Room=APB E007
|Date=2025-06-23
|DS=DS2
|Download=DBT2025-Lecture-16-overlay.pdf, DBT2025-Lecture-16-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Dependencies
|Room=APB E005
|Date=2025-06-24
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=10. Datalog Evaluation
|Room=APB E005
|Date=2025-06-24
|DS=DS5
|Download=DBT-2025-Exercise-10.pdf, DBT-2025-Exercise-10-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The Chase
|Room=APB E007
|Date=2025-06-30
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No lecture
|Room=APB E005
|Date=2025-07-01
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=11. Graph Databases and Path Queries
|Room=APB E005
|Date=2025-07-01
|DS=DS5
|Download=DBT-2025-Exercise-11.pdf, DBT-2025-Exercise-11-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The Chase (continued; termination and acyclicity)
|Room=APB E007
|Date=2025-07-07
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Answering Beyond Acyclic TGDs
|Room=APB E005
|Date=2025-07-08
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=12. Dependencies
|Room=APB E005
|Date=2025-07-08
|DS=DS5
|Download=DBT-2025-Exercise-12.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Outlook/Summary
|Room=APB E007
|Date=2025-07-14
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Konsultation
|Title=Consultation (time for your questions)
|Room=APB E005
|Date=2025-07-15
|DS=DS2
}}

Datei:DBT-2025-Exercise-12.pdf

2025-07-01T14:50:19Z

Lukas Gerlach:

Datei:DBT-2025-Exercise-11-Slides.pdf

2025-07-01T14:48:33Z

Lukas Gerlach:

Datei:DBT-2025-Exercise-10-Slides.pdf

2025-07-01T14:48:08Z

Lukas Gerlach: Lukas Gerlach lud eine neue Version von Datei:DBT-2025-Exercise-10-Slides.pdf hoch

LogAI-Seminar-2025-07-03

2025-07-01T05:08:54Z

Lukas Gerlach:

{{Veranstaltung
|Titel EN=Non-Monotonic S4F Standpoint Logic
|Beschreibung EN=Standpoint logics offer unified modal logic-based formalisms for representing multiple heterogeneous viewpoints. At the same time, many non-monotonic reasoning frameworks can be naturally captured using modal logics — in particular using the modal logic S4F. In this work, we propose a novel formalism called S4F Standpoint Logic, which generalizes both S4F and standpoint propositional logic and is therefore capable of expressing multi-viewpoint, non-monotonic semantic commitments. We define its syntax and semantics and analyze its computational complexity, obtaining the result that S4F Standpoint Logic is not computationally harder than its constituent logics, whether in monotonic or non-monotonic form. We also outline mechanisms for credulous and skeptical acceptance and illustrate the framework with a worked example.
|Veranstaltungsart=Vortrag
|Start=2025-07-03 11:00:00
|Ende=2025-07-03 12:00:00
|Raum=APB 3027
|Vortragender=Piotr Gorczyca
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Datei:ITP-2025-Paper-116-Camera-Ready.pdf

2025-06-26T13:29:17Z

Lukas Gerlach: Lukas Gerlach lud eine neue Version von Datei:ITP-2025-Paper-116-Camera-Ready.pdf hoch

Datei:ITP-2025-Paper-116-Camera-Ready.pdf

2025-06-26T13:27:14Z

Lukas Gerlach: Lukas Gerlach lud eine neue Version von Datei:ITP-2025-Paper-116-Camera-Ready.pdf hoch

Inproceedings3417

2025-06-26T13:20:29Z

Lukas Gerlach: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Johannes |ErsterAutorNachname=Tantow |FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch }} {{Inproceedings |Referiert=1 |Title=Verifying Datalog Reasoning with Lean |To appear=1 |Year=2025 |Month=September |Booktitle=ITP 2025 }} {{Publikation Details |Abstract=Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog w…“

{{Publikation Erster Autor
|ErsterAutorVorname=Johannes
|ErsterAutorNachname=Tantow
|FurtherAuthors=Lukas Gerlach; Stephan Mennicke; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Verifying Datalog Reasoning with Lean
|To appear=1
|Year=2025
|Month=September
|Booktitle=ITP 2025
}}
{{Publikation Details
|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.
|Download=ITP-2025-Paper-116-Camera-Ready.pdf
|Link=https://github.com/knowsys/CertifyingDatalog
|Projekt=Cfaed, CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}

Datei:ITP-2025-Paper-116-Camera-Ready.pdf

2025-06-26T13:18:52Z

Lukas Gerlach:

Database Theory (SS2025)

2025-06-24T14:32:09Z

Lukas Gerlach:

{{Vorlesung
|Title=Database Theory
|Research group=Wissensbasierte Systeme
|Lecturers=Markus Krötzsch
|Tutors=Lukas Gerlach
|Term=SS
|Year=2025
|Lecture series=Database Theory
|Matrix=#dbt2025:tu-dresden.de
|Module=CMS-LM-ADV, CMS-LM-MOC, INF-B-510, INF-B-520, INF-BAS6, INF-PM-FOR, INF-VERT6, MCL-KR, MCL-PI, MCL-TCSL
|SWSLecture=4
|SWSExercise=2
|SWSPractical=0
|Exam type=mündliche Prüfung
|Description=Databases are a key technology in computer science that brings together fascinating theoretical topics and highly relevant practical applications. The goal of this lecture is to give an extended introduction to this interesting field, with a special focus on database query languages, their expressive power, and computational complexity. The lecture will introduce the relational data model, and then discuss theoretical and practical aspects of a variety of query languages:

* first-order logic as a query language and the relational algebra
* conjunctive queries and their unions
* navigational queries: path queries
* Datalog and its relatives
* query answering under database dependencies

The lecture focuses on core principles that apply to many types of databases alike (relational, graph-based, semantic web). Some important query answering algorithms are presented, too, but otherwise, the details of database implementation and administration are not covered.

===Prerequisites===

Undergraduate-level knowledge of predicate logic, regular languages, and algorithmic and computational complexity is required. The lecture will connect with other topics in the Computer Science and Computational Logic curriculum, such as relational databases, logic programming, and Semantic Web technologies – familiarity with these topics is not required to follow the lecture.

===Schedule and Location===

* The weekly lecture sessions will take place on Mondays from 09:20 to 10:50 in room [[APB E007]] and Tuesdays from 09:20 to 10:50 in room [[APB E005]].
* The weekly exercise session will take place on Tuesdays from 14:50 to 16:20 in room [[APB E005]].
* The first exercise session will be on Tuesday, 2025-04-15.

===Examinations===
Dates for oral exams will be announced in due time.
As usual, you should book a date with our [mailto:secretary_wbs@mailbox.tu-dresden.de secretary] after you have officially enrolled in your respective examination office/system.

===Legacy===

This course has first been taught at TU Dresden by Prof. Dr. [[Markus Krötzsch]] in the form of the 2015 lecture [[Foundations_of_Databases_and_Query_Languages_(SS2015)/en|Foundations of Databases and Query Languages]], and later in the [[Database_Theory/en|Database Theory]] lecture series. The plan for this year's course will be somewhat similar.

The structure of some of the lectures of this course is inspired by the course ''Theory of Data and Knowledge Bases'' in the version given by [https://www.cs.ox.ac.uk/people/georg.gottlob/ Georg Gottlob] and [http://www.cs.ox.ac.uk/people/thomas.lukasiewicz/ Thomas Lukasiewicz] at the University of Oxford.
|Literature=The main reference textbook for the lecture is:
* Serge Abiteboul, Richard Hull, Victor Vianu: Foundations of Databases. Addison-Wesley. 1994.
: ''The book is available for free from [http://webdam.inria.fr/Alice/ its webpage], but there are also copies in the library.''

Further texts might be consulted for background information and additional details:
* Michael Sipser: Introduction to the Theory of Computation. 2005
: ''Accessible introduction to complexity theory that covers all topics of computational complexity that the lecture touches upon.''
* Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov: Complexity and expressive power of logic programming. ACM Computing Surveys, 33:3, pp 374-425, 2001.
: ''Covers all Datalog complexity results mentioned in the lecture. Available at http://dx.doi.org/10.1145/502807.502810 (may require access from within a university network)''
* ''additional references may be added in the course of the lecture''
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction/Relational Data Model
|Room=APB E007
|Date=2025-04-07
|DS=DS2
|Download=DBT2025-Lecture-01-overlay.pdf, DBT2025-Lecture-01-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=First-Order Queries
|Room=APB E005
|Date=2025-04-08
|DS=DS2
|Download=DBT2025-Lecture-02-overlay.pdf, DBT2025-Lecture-02-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Complexity of Query Answering
|Room=APB E007
|Date=2025-04-14
|DS=DS2
|Download=DBT2025-Lecture-03-overlay.pdf, DBT2025-Lecture-03-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Complexity of FO Query Answering
|Room=APB E005
|Date=2025-04-15
|DS=DS2
|Download=DBT2025-Lecture-04-overlay.pdf, DBT2025-Lecture-04-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=1. Relational Algebra
|Room=APB E005
|Date=2025-04-15
|DS=DS5
|Download=DBT-2025-Exercise-01.pdf, DBT-2025-Exercise-01-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Easter Monday
|Room=APB E007
|Date=2025-04-21
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Data Complexity of FO Query Answering
|Room=APB E005
|Date=2025-04-22
|DS=DS2
|Download=DBT2025-Lecture-05-overlay.pdf, DBT2025-Lecture-05-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=2. First-Order Queries
|Room=APB E005
|Date=2025-04-22
|DS=DS5
|Download=DBT-2025-Exercise-02.pdf, DBT-2025-Exercise-02-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Conjunctive Queries
|Room=APB E007
|Date=2025-04-28
|DS=DS2
|Download=DBT2025-Lecture-06-overlay.pdf, DBT2025-Lecture-06-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Tree-Like Conjunctive Queries (1)
|Room=APB E005
|Date=2025-04-29
|DS=DS2
|Download=DBT2025-Lecture-07-overlay.pdf, DBT2025-Lecture-07-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=3. Complexity of First-Order Queries
|Room=APB E005
|Date=2025-04-29
|DS=DS5
|Download=DBT-2025-Exercise-03.pdf, DBT-2025-Exercise-03-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Tree-Like Conjunctive Queries (2)
|Room=APB E007
|Date=2025-05-05
|DS=DS2
|Download=DBT2025-Lecture-08-overlay.pdf, DBT2025-Lecture-08-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Optimisation
|Room=APB E005
|Date=2025-05-06
|DS=DS2
|Download=DBT2025-Lecture-09-overlay.pdf, DBT2025-Lecture-09-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=4. Conjunctive Queries, CSP, and Hypergraphs
|Room=APB E005
|Date=2025-05-06
|DS=DS5
|Download=DBT-2025-Exercise-04.pdf, DBT-2025-Exercise-04-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Conjunctive Query Optimisation
|Room=APB E007
|Date=2025-05-12
|DS=DS2
|Download=DBT2025-Lecture-10-overlay.pdf, DBT2025-Lecture-10-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness
|Room=APB E005
|Date=2025-05-13
|DS=DS2
|Download=DBT2025-Lecture-11-overlay.pdf, DBT2025-Lecture-11-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=5. Tree Width and Hypertree Width
|Room=APB E005
|Date=2025-05-13
|DS=DS5
|Download=DBT-2025-Exercise-05.pdf, DBT-2025-Exercise-05-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness (continued)
|Room=APB E007
|Date=2025-05-19
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Expressiveness (continued)
|Room=APB E005
|Date=2025-05-20
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=6. Trakhtenbrot's Theorem
|Room=APB E005
|Date=2025-05-20
|DS=DS5
|Download=DBT-2025-Exercise-06.pdf, DBT-2025-Exercise-06-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction to Datalog / Datalog Complexity
|Room=APB E007
|Date=2025-05-26
|DS=DS2
|Download=DBT2025-Lecture-12-overlay.pdf, DBT2025-Lecture-12-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction to Datalog / Datalog Complexity (continued)
|Room=APB E005
|Date=2025-05-27
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=7. FO Query Expressivity
|Room=APB E005
|Date=2025-05-27
|DS=DS5
|Download=DBT-2025-Exercise-07.pdf, DBT-2025-Exercise-07-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Expressivity and Containment
|Room=APB E007
|Date=2025-06-02
|DS=DS2
|Download=DBT2025-Lecture-13-overlay.pdf, DBT2025-Lecture-13-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Expressivity and Containment (continued)
|Room=APB E005
|Date=2025-06-03
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=8. Datalog
|Room=APB E005
|Date=2025-06-03
|DS=DS5
|Download=DBT-2025-Exercise-08.pdf, DBT-2025-Exercise-08-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Pentecost
|Room=APB E007
|Date=2025-06-09
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Lecture: Pentecost
|Room=APB E005
|Date=2025-06-10
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No Exercise: Pentecost
|Room=APB E005
|Date=2025-06-10
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Evaluation (1)
|Room=APB E007
|Date=2025-06-16
|DS=DS2
|Download=DBT2025-Lecture-14-overlay.pdf, DBT2025-Lecture-14-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Datalog Evaluation (2) / Graph Databases
|Room=APB E005
|Date=2025-06-17
|DS=DS2
|Download=DBT2025-Lecture-15-overlay.pdf, DBT2025-Lecture-15-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=9. Semi-Positive Datalog
|Room=APB E005
|Date=2025-06-17
|DS=DS5
|Download=DBT-2025-Exercise-09.pdf, DBT-2025-Exercise-09-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Path Queries
|Room=APB E007
|Date=2025-06-23
|DS=DS2
|Download=DBT2025-Lecture-16-overlay.pdf, DBT2025-Lecture-16-print.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Dependencies
|Room=APB E005
|Date=2025-06-24
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=10. Datalog Evaluation
|Room=APB E005
|Date=2025-06-24
|DS=DS5
|Download=DBT-2025-Exercise-10.pdf, DBT-2025-Exercise-10-Slides.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The Chase
|Room=APB E007
|Date=2025-06-30
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Entfällt
|Title=No lecture
|Room=APB E005
|Date=2025-07-01
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=11. Graph Databases and Path Queries
|Room=APB E005
|Date=2025-07-01
|DS=DS5
|Download=DBT-2025-Exercise-11.pdf
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=The Chase (continued; termination and acyclicity)
|Room=APB E007
|Date=2025-07-07
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Query Answering Beyond Acyclic TGDs
|Room=APB E005
|Date=2025-07-08
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=12. Dependencies
|Room=APB E005
|Date=2025-07-08
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Outlook/Summary
|Room=APB E007
|Date=2025-07-14
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Konsultation
|Title=Consultation (time for your questions)
|Room=APB E005
|Date=2025-07-15
|DS=DS2
}}

Datei:DBT-2025-Exercise-11.pdf

2025-06-24T14:32:06Z

Lukas Gerlach: