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

Datei:TGD2026.pdf

2026-02-27T15:45:00Z

Alex Ivliev: Alex Ivliev lud eine neue Version von Datei:TGD2026.pdf hoch

Paper "Declarative Debugging for Datalog with Aggregation" for the TGD workshop 2026

Inproceedings3462

2026-02-26T14:08:38Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Raimund |ErsterAutorNachname=Dachselt |FurtherAuthors=Lukas Gerlach; Philipp Hanisch; Alex Ivliev; Markus Krötzsch; Maximilian Marx; Julián Méndez }} {{Inproceedings |Referiert=1 |Title=Declarative Debugging for Datalog with Aggregation |To appear=1 |Year=2026 |Booktitle=Proceedings of the Workshops of the EDBT/ICDT 2026 Joint Conference (EDBT/ICDT-WS 2026), Tampere, Finland, March 24, 2026 |Publisher=CEUR…“

{{Publikation Erster Autor
|ErsterAutorVorname=Raimund
|ErsterAutorNachname=Dachselt
|FurtherAuthors=Lukas Gerlach; Philipp Hanisch; Alex Ivliev; Markus Krötzsch; Maximilian Marx; Julián Méndez
}}
{{Inproceedings
|Referiert=1
|Title=Declarative Debugging for Datalog with Aggregation
|To appear=1
|Year=2026
|Booktitle=Proceedings of the Workshops of the EDBT/ICDT 2026 Joint Conference (EDBT/ICDT-WS 2026), Tampere, Finland, March 24, 2026
|Publisher=CEUR-WS.org
|Editor=Alexander Krause, João Felipe Pimentel
|Series=CEUR Workshop Proceedings
}}
{{Publikation Details
|Abstract=We propose summary proof trees as a way for explaining derivations in Datalog programs with aggregation. These combine structurally
similar parts of proof trees into a single, easier to understand structure. We show how to query for such summaries, discuss the
implementation in our rule engine Nemo, and empirically establish the feasibility of the method. We also briefly introduce a graphical
interface for editing these proof queries and visualising the results.
|Download=TGD2026.pdf
|Projekt=CPEC, CeTI, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Datei:TGD2026.pdf

2026-02-26T14:08:33Z

Alex Ivliev: Paper "Declarative Debugging for Datalog with Aggregation" for the TGD workshop 2026

Paper "Declarative Debugging for Datalog with Aggregation" for the TGD workshop 2026

Inproceedings3461

2026-02-25T12:41:41Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Markus Krötzsch; Maximilian Marx
}}
{{Inproceedings
|Referiert=1
|Title=SPARQLing Datalog for Rule-Based Reasoning over Large Knowledge Graphs
|To appear=1
|Year=2026
|Booktitle=Semantic Web - 23rd International Conference, ESWC 2026, Dubrovnik, Croatia, May 10 - 14, 2026, Proceedings
|Publisher=Springer
|Editor=Maribel Acosta, Marieke van Erp, Sebastian Rudolph, Olaf Hartig, Blerina Spahiu, Anisa Rula, Daniel Garijo, Francesco Osborne
|Series=Lecture Notes in Computer Science
|Note=To appear
}}
{{Publikation Details
|Projekt=CPEC, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3461

2026-02-25T12:41:21Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Markus Krötzsch; Maximilian Marx
}}
{{Inproceedings
|Referiert=1
|Title=SPARQLing Datalog for Rule-Based Reasoning over Large Knowledge Graphs
|To appear=1
|Year=2026
|Booktitle=Semantic Web - 23rd International Conference, ESWC 2026, Dubrovnik, Croatia, May 10 - 14, 2026, Proceedings
|Publisher=Springer
|Editor=Maribel Acosta, Marieke van Erp, Sebastian Rudolph, Olaf Hartig, Blerina Spahiu, Anisa Rula, Daniel Garijo, Francesco Osborne
|Series=Lecture Notes in Computer Science
}}
{{Publikation Details
|Projekt=CPEC, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3461

2026-02-25T12:29:31Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Markus Krötzsch; Maximilian Marx
}}
{{Inproceedings
|Referiert=1
|Title=SPARQLing Datalog for Rule-Based Reasoning over Large Knowledge Graphs
|To appear=1
|Year=2026
|Booktitle=The Semantic Web - 23rd European Semantic Web Conference, ESWC 2026, Dubrovnik, Croatia, May 10-14, 2026, Proceedings
|Publisher=Springer
|Editor=Maribel Acosta, Marieke van Erp, Sebastian Rudolph, Olaf Hartig, Blerina Spahiu, Anisa Rula, Daniel Garijo, Francesco Osborne
|Series=Lecture Notes in Computer Science
}}
{{Publikation Details
|Projekt=CPEC, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3461

2026-02-25T12:28:53Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Alex |ErsterAutorNachname=Ivliev |FurtherAuthors=Markus Krötzsch; Maximilian Marx }} {{Inproceedings |Referiert=1 |Title=SPARQLing Datalog for Rule-Based Reasoning over Large Knowledge Graphs |To appear=1 |Year=2026 |Booktitle=The Semantic Web - 23rd European Semantic Web Conference, {ESWC} 2026, Dubrovnik, Croatia, May 10-14, 2026, Proceedings |Publisher=Springer |Editor=Maribel Acosta, Marieke van Erp, Seb…“

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Markus Krötzsch; Maximilian Marx
}}
{{Inproceedings
|Referiert=1
|Title=SPARQLing Datalog for Rule-Based Reasoning over Large Knowledge Graphs
|To appear=1
|Year=2026
|Booktitle=The Semantic Web - 23rd European Semantic Web Conference, {ESWC} 2026, Dubrovnik, Croatia, May 10-14, 2026, Proceedings
|Publisher=Springer
|Editor=Maribel Acosta, Marieke van Erp, Sebastian Rudolph, Olaf Hartig, Blerina Spahiu, Anisa Rula, Daniel Garijo, Francesco Osborne
|Series=Lecture Notes in Computer Science
}}
{{Publikation Details
|Projekt=CPEC, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Article3119

2026-02-19T16:27:00Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Article
|Referiert=1
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=0
|Year=2026
|Month=Februar
|Journal=Theory and Practice of Logic Programming
|Pages=1-23
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|Download=Towards-mass-spectrum-analysis-with-asp.pdf
|DOI Name=10.1017/S1471068426100398
|Projekt=CPEC, CeTI, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Article3119

2026-02-19T16:26:38Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Article
|Referiert=1
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=0
|Year=2026
|Month=Februar
|Journal=Theory and Practice of Logic Programming
|Pages=1--23
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|Download=Towards-mass-spectrum-analysis-with-asp.pdf
|DOI Name=10.1017/S1471068426100398
|Projekt=CPEC, CeTI, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Article3119

2026-02-19T16:26:02Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Article
|Referiert=1
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=0
|Year=2026
|Month=Februar
|Journal=Theory and Practice of Logic Programming
|Pages=1--23
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|Download=Towards-mass-spectrum-analysis-with-asp.pdf
|DOI Name=https://doi.org/10.1017/S1471068426100398
|Projekt=CPEC, CeTI, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

News105

2025-05-13T07:51:29Z

Alex Ivliev:

{{Neuigkeit
|Titel DE=Franz Baader und Renata Wassermann gewinnen Ray Reiter Best Paper Award bei der KR 2024
|Titel EN=Franz Baader and Renata Wassermann Win Ray Reiter Best Paper Award at KR 2024
|Beschreibung DE=Die renommierten Informatiker [[Franz Baader]] (Technische Universität Dresden) und Renata Wassermann (Universidade de São Paulo) wurden auf der [https://kr.org/KR2024 21. International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)] mit dem Ray Reiter Best Paper Award für ihre Arbeit mit dem Titel [https://proceedings.kr.org/2024/9/kr2024-0009-baader-et-al.pdf "Contractions Based on Optimal Repairs"] ausgezeichnet.
In ihrer Publikation nutzen Baader und Wassermann neueste Fortschritte bei der Charakterisierung und Berechnung optimaler Reparaturen für Ontologien auf Basis von Beschreibungslogiken, um Kontraktionsoperationen zu entwickeln, die die Vorteile von Belief Set und Belief Base Kontraktionen vereinen.
Diese Auszeichnung unterstreicht die anhaltende Relevanz grundlegender Forschung im Bereich der logikbasierten Künstlichen Intelligenz und bestätigt die einflussreiche Rolle der Autoren in der Weiterentwicklung von Theorie und Praxis der Wissensrepräsentation.
|Beschreibung EN=Distinguished computer scientists [[Franz Baader]] (Technische Universität Dresden) and Renata Wassermann (Universidade de São Paulo) have been awarded the Ray Reiter Best Paper Award at the [https://kr.org/KR2024 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)] for their work titled [https://proceedings.kr.org/2024/9/kr2024-0009-baader-et-al.pdf "Contractions Based on Optimal Repairs"].
In their paper, Baader and Wassermann leverage recent advances in characterizing and computing optimal repairs for ontologies based on Description Logics to obtain contraction operations that combine the advantages of belief sets and balief base contractions.
The recognition highlights the continuing relevance of foundational research in logic-based AI and reaffirms the authors' influential roles in shaping the theory and practice of knowledge representation.
|URL=https://proceedings.kr.org/2024/9/kr2024-0009-baader-et-al.pdf
|Datum=2024/11/25
|Bild=KR2024 BestPaperAward Ceremony.jpg
|Forschungsgruppe=Automatentheorie
}}

News105/en

2025-05-13T07:50:43Z

Alex Ivliev: Page created automatically by parser function on page News105

News105

2025-05-13T07:50:43Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Franz Baader und Renata Wassermann gewinnen Ray Reiter Best Paper Award bei der KR 2024 |Titel EN=Franz Baader and Renata Wassermann Win Ray Reiter Best Paper Award at KR 2024 |Beschreibung DE=Die renommierten Informatiker Franz Baader (Technische Universität Dresden) und Renata Wassermann (Universidade de São Paulo) wurden auf der [https://kr.org/KR2024 "21. International Conference on Principles of Knowledge Representation…“

{{Neuigkeit
|Titel DE=Franz Baader und Renata Wassermann gewinnen Ray Reiter Best Paper Award bei der KR 2024
|Titel EN=Franz Baader and Renata Wassermann Win Ray Reiter Best Paper Award at KR 2024
|Beschreibung DE=Die renommierten Informatiker [[Franz Baader]] (Technische Universität Dresden) und Renata Wassermann (Universidade de São Paulo) wurden auf der [https://kr.org/KR2024 "21. International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)"] mit dem Ray Reiter Best Paper Award für ihre Arbeit mit dem Titel [https://proceedings.kr.org/2024/9/kr2024-0009-baader-et-al.pdf "Contractions Based on Optimal Repairs"] ausgezeichnet.
In ihrer Publikation nutzen Baader und Wassermann neueste Fortschritte bei der Charakterisierung und Berechnung optimaler Reparaturen für Ontologien auf Basis von Beschreibungslogiken, um Kontraktionsoperationen zu entwickeln, die die Vorteile von Belief Set und Belief Base Kontraktionen vereinen.
Diese Auszeichnung unterstreicht die anhaltende Relevanz grundlegender Forschung im Bereich der logikbasierten Künstlichen Intelligenz und bestätigt die einflussreiche Rolle der Autoren in der Weiterentwicklung von Theorie und Praxis der Wissensrepräsentation.
|Beschreibung EN=Distinguished computer scientists [[Franz Baader]] (Technische Universität Dresden) and Renata Wassermann (Universidade de São Paulo) have been awarded the Ray Reiter Best Paper Award at the [https://kr.org/KR2024 "21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)"] for their work titled [https://proceedings.kr.org/2024/9/kr2024-0009-baader-et-al.pdf "Contractions Based on Optimal Repairs"].
In their paper, Baader and Wassermann leverage recent advances in characterizing and computing optimal repairs for ontologies based on Description Logics to obtain contraction operations that combine the advantages of belief sets and balief base contractions.
The recognition highlights the continuing relevance of foundational research in logic-based AI and reaffirms the authors' influential roles in shaping the theory and practice of knowledge representation.
|URL=https://proceedings.kr.org/2024/9/kr2024-0009-baader-et-al.pdf
|Datum=2024/11/25
|Bild=KR2024 BestPaperAward Ceremony.jpg
|Forschungsgruppe=Automatentheorie
}}

Datei:KR2024 BestPaperAward Ceremony.jpg

2025-05-13T07:44:39Z

Alex Ivliev:

News104

2025-01-20T13:50:08Z

Alex Ivliev:

{{Neuigkeit
|Titel DE=ICCL Forschende tragen zur Lean-Standardbibliothek bei
|Titel EN=ICCL Researchers Contribute to Lean Standard Library
|Beschreibung DE=Johannes Tantow (ehemaliger Student der Gruppe [[Wissensbasierte Systeme]]; jetzt wissenschaftlicher Mitarbeiter an der TU Chemnitz) und [[Lukas Gerlach]] (Wissenschaftlicher Mitarbeiter der Gruppe [[Wissensbasierte Systeme]]) haben kürzlich eine große Anzahl von Resultaten rund um Hash-Maps zur Standardbibliothek des interaktiven Theorembeweisers [https://lean-lang.org/ Lean] beigetragen. Interaktive Theorembeweiser ermöglichen das Schreiben von Beweisen in einem maschinenüberprüfbaren Format. Im Fall von Lean werden Beweise als Teil einer funktionalen Programmiersprache geschrieben.In seiner Diplomarbeit hat Johannes unter Aufsicht von Lukas, [[Stephan Mennicke]] und [[Markus Krötzsch]] ein [https://github.com/knowsys/CertifyingDatalog Tool] entwickelt, mit dem die Korrektheit von Datalog-Beweisbäumen überprüft werden kann. Dieses Tool ist in Lean geschrieben und formal verifiziert. Das heißt, wenn das Tool einen gegebenen Datalog-Beweisbaum akzeptiert, kann man sicher sein, dass der Beweisbaum tatsächlich korrekt ist. Aus Performanzgründen verwendet das Tool Hash-Maps, die bereits in der Lean-Standardbibliothek vorhanden waren, für die jedoch zu diesem Zeitpunkt nur eine Handvoll Korrektheitsergebnisse formalisiert wurden. Man möchte beispielsweise verifizieren, dass, wenn eine Hash-Map aus einer Liste von Schlüssel-Wert-Paaren erstellt wird, jeder der Schlüssel anschließend in der Hash-Map vorkommt.
Obwohl solche Ergebnisse offensichtlich erscheinen, ist es keine triviale Aufgabe, dies anhand der internen Implementierung der Hash-Map zu beweisen.In enger Zusammenarbeit mit Mitgliedern des Lean-Entwicklungsteams haben Johannes und Lukas in den letzten Wochen und Monaten viel Zeit damit verbracht, einige dieser Lücken zu schließen. Ein [https://github.com/leanprover/lean4/pull/6211 PR] zur Überprüfung von Eigenschaften rund um das Erstellen von Hash-Maps aus Listen ist gerade mit rund 5000 hinzugefügten Codezeilen in den Main-Branch übernommen worden. Diese Änderungen werden Teil der kommenden Lean-Version 4.17 sein und von Johannes und Lukas selbst verwendet werden, um das bereits vorhandene Datalog-Beweisbaum Verifizierungstool abzurunden.Sowohl Johannes als auch Lukas sind sehr zufrieden mit dem Verlauf der Zusammenarbeit. „Es war eine großartige Gelegenheit, nicht nur einige konkrete Beiträge für die Lean-Community zu leisten, sondern auch wertvolle Einblicke in die Entwicklung von Lean im großen Maßstab zu erhalten“, sagte Lukas.
|Beschreibung EN=Johannes Tantow (former student at the [[Knowledge-Based Systems]] group; now Research Associate at TU Chemnitz) and [[Lukas Gerlach]] (Research Associate at the [[Knowledge-Based Systems]] group) have recently contributed a sizable number of results around hash maps to the standard library of the interactive theorem prover [https://lean-lang.org/ Lean]. Interactive theorem provers allow to write proofs in a machine-verifiable format. In the case of Lean, proofs are written as part of a functional programming language.In his Diploma Thesis, Johannes, under supervision of Lukas, [[Stephan Mennicke]], and [[Markus Krötzsch]], built a [https://github.com/knowsys/CertifyingDatalog tool] that is able to check correctness of Datalog proof trees. This tool is written and formally verified in Lean. That is, if the tool accepts a given Datalog proof tree, we can be certain that the proof tree is indeed correct. For performance reasons, this tool is using hash map data structures, which already existed in the Lean standard library but only a handful of correctness results had been formalized at the time.
For example, one would like to verify that if a hash map is built from a list of key-value pairs, then each of the keys occurs in the hash map afterwards. While such results seem obvious, it is a non-trivial task to prove this over the internal implementation of the hash map.In close collaboration with members of the Lean development team, Johannes and Lukas spent some time throughout the last weeks and months to fill in some of these gaps. A [https://github.com/leanprover/lean4/pull/6211 PR] verifying properties around building hash maps from lists just landed on the main branch with around 5000 lines of code added. These changes will be part of the upcoming Lean version 4.17 and be used by Johannes and Lukas themselves to round up the already existing Datalog proof tree verification tool.Both Johannes and Lukas are very happy with how the collaboration went. "It was a great opportunity to not only make some tangible contributions for the Lean community but also to obtain valuable insights about developing Lean at scale", Lukas said.
|Datum=2025/01/20
|Bild=News Lean.png
|Forschungsgruppe=Knowledge-Based Systems
}}

News104/en

2025-01-20T13:47:58Z

Alex Ivliev: Page created automatically by parser function on page News104

News104

2025-01-20T13:47:58Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=ICCL Forschende tragen zur Lean-Standardbibliothek bei |Titel EN=ICCL Researchers Contribute to Lean Standard Library |Beschreibung DE=Johannes Tantow (ehemaliger Student der Gruppe Wissensbasierte Systeme; jetzt wissenschaftlicher Mitarbeiter an der TU Chemnitz) und Lukas Gerlach (Wissenschaftlicher Mitarbeiter der Gruppe Wissensbasierte Systeme) haben kürzlich eine große Anzahl von Resultaten rund um Hash-Maps zur Standard…“

{{Neuigkeit
|Titel DE=ICCL Forschende tragen zur Lean-Standardbibliothek bei
|Titel EN=ICCL Researchers Contribute to Lean Standard Library
|Beschreibung DE=Johannes Tantow (ehemaliger Student der Gruppe Wissensbasierte Systeme; jetzt wissenschaftlicher Mitarbeiter an der TU Chemnitz) und [[Lukas Gerlach]] (Wissenschaftlicher Mitarbeiter der Gruppe Wissensbasierte Systeme) haben kürzlich eine große Anzahl von Resultaten rund um Hash-Maps zur Standardbibliothek des interaktiven Theorembeweisers [https://lean-lang.org/ Lean] beigetragen. Interaktive Theorembeweiser ermöglichen das Schreiben von Beweisen in einem maschinenüberprüfbaren Format. Im Fall von Lean werden Beweise als Teil einer funktionalen Programmiersprache geschrieben.In seiner Diplomarbeit hat Johannes unter Aufsicht von Lukas, [[Stephan Mennicke]] und [[Markus Krötzsch]] ein [https://github.com/knowsys/CertifyingDatalog Tool] entwickelt, mit dem die Korrektheit von Datalog-Beweisbäumen überprüft werden kann. Dieses Tool ist in Lean geschrieben und formal verifiziert. Das heißt, wenn das Tool einen gegebenen Datalog-Beweisbaum akzeptiert, kann man sicher sein, dass der Beweisbaum tatsächlich korrekt ist. Aus Performanzgründen verwendet das Tool Hash-Maps, die bereits in der Lean-Standardbibliothek vorhanden waren, für die jedoch zu diesem Zeitpunkt nur eine Handvoll Korrektheitsergebnisse formalisiert wurden. Man möchte beispielsweise verifizieren, dass, wenn eine Hash-Map aus einer Liste von Schlüssel-Wert-Paaren erstellt wird, jeder der Schlüssel anschließend in der Hash-Map vorkommt.
Obwohl solche Ergebnisse offensichtlich erscheinen, ist es keine triviale Aufgabe, dies anhand der internen Implementierung der Hash-Map zu beweisen.In enger Zusammenarbeit mit Mitgliedern des Lean-Entwicklungsteams haben Johannes und Lukas in den letzten Wochen und Monaten viel Zeit damit verbracht, einige dieser Lücken zu schließen. Ein [https://github.com/leanprover/lean4/pull/6211 PR] zur Überprüfung von Eigenschaften rund um das Erstellen von Hash-Maps aus Listen ist gerade mit rund 5000 hinzugefügten Codezeilen in den Main-Branch übernommen worden. Diese Änderungen werden Teil der kommenden Lean-Version 4.17 sein und von Johannes und Lukas selbst verwendet werden, um das bereits vorhandene Datalog-Beweisbaum Verifizierungstool abzurunden.Sowohl Johannes als auch Lukas sind sehr zufrieden mit dem Verlauf der Zusammenarbeit. „Es war eine großartige Gelegenheit, nicht nur einige konkrete Beiträge für die Lean-Community zu leisten, sondern auch wertvolle Einblicke in die Entwicklung von Lean im großen Maßstab zu erhalten“, sagte Lukas.
|Beschreibung EN=Johannes Tantow (former student at the Knowledge-Based Systems group; now Research Associate at TU Chemnitz) and [[Lukas Gerlach]] (Research Associate at the Knowledge-Based Systems group) have recently contributed a sizable number of results around hash maps to the standard library of the interactive theorem prover [https://lean-lang.org/ Lean]. Interactive theorem provers allow to write proofs in a machine-verifiable format. In the case of Lean, proofs are written as part of a functional programming language.In his Diploma Thesis, Johannes, under supervision of Lukas, [[Stephan Mennicke]], and [[Markus Krötzsch]], built a [https://github.com/knowsys/CertifyingDatalog tool] that is able to check correctness of Datalog proof trees. This tool is written and formally verified in Lean. That is, if the tool accepts a given Datalog proof tree, we can be certain that the proof tree is indeed correct. For performance reasons, this tool is using hash map data structures, which already existed in the Lean standard library but only a handful of correctness results had been formalized at the time.
For example, one would like to verify that if a hash map is built from a list of key-value pairs, then each of the keys occurs in the hash map afterwards. While such results seem obvious, it is a non-trivial task to prove this over the internal implementation of the hash map.In close collaboration with members of the Lean development team, Johannes and Lukas spent some time throughout the last weeks and months to fill in some of these gaps. A [https://github.com/leanprover/lean4/pull/6211 PR] verifying properties around building hash maps from lists just landed on the main branch with around 5000 lines of code added. These changes will be part of the upcoming Lean version 4.17 and be used by Johannes and Lukas themselves to round up the already existing Datalog proof tree verification tool.Both Johannes and Lukas are very happy with how the collaboration went. "It was a great opportunity to not only make some tangible contributions for the Lean community but also to obtain valuable insights about developing Lean at scale", Lukas said.
|Datum=2025/01/20
|Bild=News Lean.png
|Forschungsgruppe=Knowledge-Based Systems
}}

Datei:News Lean.png

2025-01-20T13:37:20Z

Alex Ivliev: Lean code shown in the news item about Johannes' and Lukas' contribution

Lean code shown in the news item about Johannes' and Lukas' contribution

News103/en

2024-12-13T12:23:58Z

Alex Ivliev: Page created automatically by parser function on page News103

News103

2024-12-13T12:23:58Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Jonas Karge gewinnt Student Best Paper Award auf der PRIMA24 |Titel EN=Jonas Karge Wins Student Best Paper Award at PRIMA24 |Beschreibung DE=Jonas Karge, Doktorand am Lehrstuhl für Computational Logic am Institut für Theoretische Informatik der TU Dresden, wurde auf der diesjährigen [https://sites.google.com/view/prima-2024/ International Conference on Principles and Practice of Multi-Agent Systems (PRIMA24)] in Kyoto,…“

{{Neuigkeit
|Titel DE=Jonas Karge gewinnt Student Best Paper Award auf der PRIMA24
|Titel EN=Jonas Karge Wins Student Best Paper Award at PRIMA24
|Beschreibung DE=[[Jonas Karge]], Doktorand am Lehrstuhl für [[Computational Logic]] am Institut für Theoretische Informatik der TU Dresden, wurde auf der diesjährigen [https://sites.google.com/view/prima-2024/ International Conference on Principles and Practice of Multi-Agent Systems (PRIMA24)] in Kyoto, Japan, mit dem Martin Purvis Student Best Paper Award für seinen Beitrag [https://iccl.inf.tu-dresden.de/web/Inproceedings3394 „Taming Dilation in Imprecise Pooling“] ausgezeichnet.In dieser Arbeit entwickelte Jonas die erste Formalisierung von Dilation für den Fall, dass die unpräzisen bzw. intervallwertigen probabilistischen Überzeugungen mehrerer Agenten aggregiert werden. Dilation ist eines der wichtigsten Probleme im Zusammenhang mit unpräzisen Wahrscheinlichkeiten und beschreibt das Phänomen, dass die Hinzunahme neuer Informationen in einigen Fällen zwangsläufig zu einer Zunahme von Unsicherheit führen kann. Darüber hinaus beschreibt das Papier die genauen Bedingungen, unter denen Dilation zu erwarten ist und in welchem Ausmaß diese stattfindet. Dies basiert auf einem kürzlich vorgeschlagenen Aggregationsschema für ungenaue Wahrscheinlichkeiten, der als Voting for Bins bezeichnet wird.Die PRIMA ist eine wichtige Konferenz im Bereich Multiagentensysteme, welche dieses Jahr ihr 25-jähriges Bestehen feierte. Auf der Konferenz gibt es sowohl theoretische als auch angewandte Beiträge zu Multi-Agenten Systemen. Dabei handelt es sich um Systeme, in denen autonome Agenten in einer gemeinsamen Umgebung unabhängig von einander Entscheidungen treffen können. In der diesjährigen Ausgabe von PRIMA wurden insbesondere Beiträge zu Koordination und Kooperation, zu logischen Aspekten von Multiagentensystemen sowie Computational Social Choice vorgestellt.Herzlichen Glückwunsch!
|Beschreibung EN=[[Jonas Karge]], PhD student at the chair of [[Computational Logic]] at the Institute of Theoretical Computer Science, TU Dresden, was awarded the Martin Purvis Student Best Paper Award for his contribution [https://iccl.inf.tu-dresden.de/web/Inproceedings3394/en „Taming Dilation in Imprecise Pooling“] at this year’s edition of the [https://sites.google.com/view/prima-2024/ International Conference on Principles and Practice of Multi-Agent Systems (PRIMA24)] in Kyoto, Japan.In this paper, Jonas Karge developed the first formal treatment of dilation for the case where the imprecise or interval-valued probabilistic beliefs of multiple agents are aggregated. Dilation is one of the most important concerns associated with imprecise probabilities in general, and describes the phenomenon that, in some cases, the acquisition of new information inevitably leads to an increase in uncertainty. Furthermore, the paper describes the precise conditions under which and to what extent dilation is expected to occur, using a recently proposed aggregation framework for imprecise probabilities, referred to as Voting for Bins.PRIMA is a well-established conference in the multi-agent research community and celebrated its 25th edition in 2024. It invites both theoretical and applied contributions in the field of multi-agent systems, the study of the interaction of autonomous agents - entities capable of independent decision making - in a shared environment. In this year's edition of PRIMA, papers on coordination and cooperation, logical aspects of multi-agent systems, and computational social choice were particularly represented.Our heartfelt congratulations on this success!
|Datum=2024/11/20
|Bild=BestPaper Jonas Kyoto.jpeg
|Forschungsgruppe=Computational Logic
}}

Datei:BestPaper Jonas Kyoto.jpeg

2024-12-13T12:15:35Z

Alex Ivliev: Bild zeigt Jonas Karge mit dem Best Paper Award

Bild zeigt Jonas Karge mit dem Best Paper Award

News102/en

2024-12-03T10:07:49Z

Alex Ivliev: Page created automatically by parser function on page News102

News102

2024-12-03T10:07:48Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Best Paper Award für Nemo |Titel EN=Best Paper Award for Nemo |Beschreibung DE=Forschende der Professur Wissensbasierte Systeme am Institut für Theoretische Informatik der TU Dresden wurden auf der renommierten [https://kr.org/KR2024/ KR-Konferenz 2024] in Hanoi, Vietnam mit dem Best-Paper-Award im Track "KR in the Wild" geehrt. Die Autoren Alex Ivliev, Lukas Gerlach, Simon Meusel, Jakob Steinberg und Marku…“

{{Neuigkeit
|Titel DE=Best Paper Award für Nemo
|Titel EN=Best Paper Award for Nemo
|Beschreibung DE=Forschende der Professur [[Wissensbasierte Systeme]] am Institut für Theoretische Informatik der TU Dresden wurden auf der renommierten [https://kr.org/KR2024/ KR-Konferenz 2024] in Hanoi, Vietnam mit dem Best-Paper-Award im Track "KR in the Wild" geehrt. Die Autoren [[Alex Ivliev]], [[Lukas Gerlach]], [[Simon Meusel]], [[Jakob Steinberg]] und [[Markus Krötzsch]] überzeugten mit ihrem Beitrag [https://iccl.inf.tu-dresden.de/web/Inproceedings3390 "Nemo: Your Friendly and Versatile Rule Reasoning Toolkit"].Das ausgezeichnete Paper beschreibt [https://github.com/knowsys/nemo Nemo] – ein Toolkit für regelbasiertes Schließen, welches besonderen Fokus auf Skalierbarkeit, Vielseitigkeit und Benutzerfreundlichkeit legt. Nemo erweitert die bekannte Regel- und Abfragesprache Datalog um zahlreiche nützliche Features wie Aggregate, existentielle Regeln und die Unterstützung zahlreicher Datentypen. Weitere Informationen und eine vollständige Dokumentation sind [https://knowsys.github.io/nemo-doc/ hier] verfügbar. Die Entwicklung von Nemo ist eng mit den Forschungsprojekten [https://www.perspicuous-computing.science CPEC], [https://www.innosale.eu InnoSale] und [https://www.secai.org SECAI] verbunden.Die [https://www.kr.org/ International Conference on Principles of Knowledge Representation and Reasoning (KR)] ist eine wichtige Fachkonferenz im Bereich der Künstlichen Intelligenz. Sie beschäftigt sich mit der Frage, wie Wissen in symbolischer Form dargestellt und mit Hilfe von Computersystemen verarbeitet werden kann. Dies ermöglicht es intelligenten Systemen, komplexe Schlüsse zu ziehen, welche aber gleichzeitig für den Menschen nachvollziehbar bleiben. Der [https://www.kr.org/KR2024/cfp_kr_in_the_wild.php „KR in the Wild“-Track] wurde in diesem Jahr erstmals eingeführt und richtete den Fokus auf die Entwicklung von regelbasierten Schließsystemen sowie deren praxisnahe Anwendungen.Herzlichen Glückwunsch an Alex, Lukas, Simon, Jakob und Markus!
|Beschreibung EN=Researchers from the Chair of [[Knowledge-Based Systems]] at the Institute of Theoretical Computer Science, TU Dresden, received the Best Paper Award in the "KR in the Wild" track at the prestigious conference [https://kr.org/KR2024/ KR 2024] in Hanoi, Vietnam. The authors [[Alex Ivliev]], [[Lukas Gerlach]], [[Simon Meusel]], [[Jakob Steinberg]], and [[Markus Krötzsch]] presented their paper [https://iccl.inf.tu-dresden.de/web/Inproceedings3390 "Nemo: Your Friendly and Versatile Rule Reasoning Toolkit"].The award-winning paper describes [https://github.com/knowsys/nemo Nemo], a powerful toolkit for rule-based reasoning that emphasizes scalability, versatility, and ease of use. Nemo extends the popular rule and query language Datalog with numerous useful features such as aggregates, existential rules, and support for various data types. More information and a complete documentation can be found [https://github.com/knowsys/nemo-doc here]. The development of Nemo is closely connected to the research projects [https://www.perspicuous-computing.science CPEC], [https://www.innosale.eu InnoSale], and [https://www.secai.org SECAI].The [https://www.kr.org International Conference on Principles of Knowledge Representation and Reasoning (KR)] is an important conference in the field of Artificial Intelligence. It focuses on the symbolic representation of knowledge that can be processed by computer systems, enabling intelligent systems to draw complex, yet humanly comprehensible, conclusions. This year, the [https://www.kr.org/KR2024/cfp_kr_in_the_wild.php "KR in the Wild" track] was introduced for the first time, spotlighting the development of rule-based reasoning systems and their practical applications.Congratulations to Alex, Lukas, Simon, Jakob, and Markus!
|Datum=2024/11/05
|Bild=Best paper nemo.jpeg
|Forschungsgruppe=Knowledge-Based Systems
}}

Datei:Best paper nemo.jpeg

2024-12-03T09:57:15Z

Alex Ivliev: Photo of Lukas, Alex, Markus holding the best paper award KR'2024 In-the-wild

Photo of Lukas, Alex, Markus holding the best paper award KR'2024 In-the-wild

Inproceedings3390

2024-11-27T08:26:08Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Lukas Gerlach; Simon Meusel; Jakob Steinberg; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Nemo: Your Friendly and Versatile Rule Reasoning Toolkit
|To appear=0
|Year=2024
|Month=November
|Booktitle=Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)
|Pages=743-754
|Publisher=IJCAI Organization
|Editor=Pierre Marquis,Magdalena Ortiz,Maurice Pagnucco
|Series=Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning
}}
{{Publikation Tool
|Tool=Nemo
}}
{{Publikation Details
|Abstract=We present Nemo, a toolkit for rule-based reasoning and data processing that emphasises robustness and ease of use. Nemo’s core is a scalable and efficient main-memory reasoner that supports an expressive extension of Datalog with support for data types, existential rules, aggregates, and (stratified) negation. Built around this core is a versatile system of libraries and applications for interfacing with several data formats and programming languages, use as a web application, and IDE integration. In this system description, we present this toolkit and discuss relevant application areas in rule-based knowledge representation, knowledge graph processing, and reasoner prototyping. Our evaluation on a range of tasks from these areas demonstrates Nemo’s robust performance in comparison to state-of-the-art rule engines.
|ISBN=978-1-956792-05-8
|ISSN=2334-1033
|Download=KR-2024-CR.pdf
|Slides=Datalog20 Ivliev Slides.pdf
|DOI Name=https://doi.org/10.24963/kr.2024/70
|Projekt=Cfaed, CPEC, InnoSale, SECAI, ScaDS.AI, Wikidata
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Wissensrepräsentation und logisches Schließen
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Semantische Technologien
}}

Inproceedings3390

2024-11-27T08:22:01Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Lukas Gerlach; Simon Meusel; Jakob Steinberg; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Nemo: Your Friendly and Versatile Rule Reasoning Toolkit
|To appear=0
|Year=2024
|Booktitle=Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)
|Pages=743-754
|Publisher=IJCAI Organization
|Series=Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning
}}
{{Publikation Tool
|Tool=Nemo
}}
{{Publikation Details
|Abstract=We present Nemo, a toolkit for rule-based reasoning and data processing that emphasises robustness and ease of use. Nemo’s core is a scalable and efficient main-memory reasoner that supports an expressive extension of Datalog with support for data types, existential rules, aggregates, and (stratified) negation. Built around this core is a versatile system of libraries and applications for interfacing with several data formats and programming languages, use as a web application, and IDE integration. In this system description, we present this toolkit and discuss relevant application areas in rule-based knowledge representation, knowledge graph processing, and reasoner prototyping. Our evaluation on a range of tasks from these areas demonstrates Nemo’s robust performance in comparison to state-of-the-art rule engines.
|Download=KR-2024-CR.pdf
|Slides=Datalog20 Ivliev Slides.pdf
|DOI Name=https://doi.org/10.24963/kr.2024/70
|Projekt=Cfaed, CPEC, InnoSale, SECAI, ScaDS.AI, Wikidata
|Forschungsgruppe=Wissensbasierte Systeme
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Existenzielle Regeln
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Regelbasiertes Schließen
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Wissensrepräsentation und logisches Schließen
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Semantische Technologien
}}

Inproceedings3393

2024-11-27T08:18:55Z

Alex Ivliev:

Inproceedings3393

2024-11-27T08:16:44Z

Alex Ivliev:

Inproceedings3392

2024-11-27T08:14:24Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Inproceedings
|Referiert=1
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=0
|Year=2024
|Month=Oktober
|Booktitle=Logic Programming and Nonmonotonic Reasoning
|Pages=200-214
|Publisher=Springer, Cham
|Editor=Carmine Dodaro, Gopal Gupta, Maria Vanina Martinez
|Series=Lecture Notes in Computer Science
|Volume=15245
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|ISBN=978-3-031-74208-8
|ISSN=0302-9743
|Download=LPNMR2024-Küchenmeister.pdf
|Slides=LPNMR2024 Kuechenmeister Slides.pdf
|Link=https://tools.iccl.inf.tu-dresden.de/genmol/
|DOI Name=https://doi.org/10.1007/978-3-031-74209-5_16
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3393

2024-10-21T14:03:39Z

Alex Ivliev:

Inproceedings3393

2024-10-21T13:58:16Z

Alex Ivliev:

Datei:Datalog20 Ivliev Slides.pdf

2024-10-21T13:58:09Z

Alex Ivliev: Slides for the presentation of Nemo at Datalog 2.0 workshop 2024

Slides for the presentation of Nemo at Datalog 2.0 workshop 2024

Inproceedings3392

2024-10-21T13:52:08Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=0
|Year=2024
|Month=Oktober
|Booktitle=Logic Programming and Nonmonotonic Reasoning
|Pages=200-214
|Publisher=Springer, Cham
|Editor=Carmine Dodaro, Gopal Gupta, Maria Vanina Martinez
|Series=Lecture Notes in Computer Science
|Volume=15245
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|ISBN=978-3-031-74208-8
|ISSN=0302-9743
|Download=LPNMR2024-Küchenmeister.pdf
|Slides=LPNMR2024 Kuechenmeister Slides.pdf
|Link=https://tools.iccl.inf.tu-dresden.de/genmol/
|DOI Name=https://doi.org/10.1007/978-3-031-74209-5_16
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3392

2024-10-21T13:48:37Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=0
|Year=2024
|Month=Oktober
|Booktitle=Logic Programming and Nonmonotonic Reasoning
|Pages=200-214
|Publisher=Springer
|Editor=Carmine Dodaro, Gopal Gupta, Maria Vanina Martinez
|Series=Lecture Notes in Computer Science
|Volume=15245
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|ISBN=978-3-031-74208-8
|ISSN=0302-9743
|Download=LPNMR2024-Küchenmeister.pdf
|Slides=LPNMR2024 Kuechenmeister Slides.pdf
|Link=https://tools.iccl.inf.tu-dresden.de/genmol/
|DOI Name=Springer
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3392

2024-10-21T13:48:13Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=1
|Year=2024
|Month=Dezember
|Booktitle=Logic Programming and Nonmonotonic Reasoning
|Pages=200-214
|Publisher=Springer
|Editor=Carmine Dodaro, Gopal Gupta, Maria Vanina Martinez
|Series=Lecture Notes in Computer Science
|Volume=15245
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|ISBN=978-3-031-74208-8
|ISSN=0302-9743
|Download=LPNMR2024-Küchenmeister.pdf
|Slides=LPNMR2024 Kuechenmeister Slides.pdf
|Link=https://tools.iccl.inf.tu-dresden.de/genmol/
|DOI Name=Springer
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Datei:LPNMR2024 Kuechenmeister Slides.pdf

2024-10-21T13:43:47Z

Alex Ivliev: Slides for the presentation of the LPNMR2024 paper about Genmol

Slides for the presentation of the LPNMR2024 paper about Genmol

Inproceedings3393/en

2024-09-13T13:57:09Z

Alex Ivliev: Page created automatically by parser function on page Inproceedings3393

#REDIRECT [[Inproceedings3393]]

Inproceedings3393

2024-09-13T13:57:09Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Alex |ErsterAutorNachname=Ivliev |FurtherAuthors=Lukas Gerlach; Simon Meusel; Jakob Steinberg; Markus Krötzsch }} {{Inproceedings |Referiert=0 |Title=Nemo: A Scalable and Versatile Datalog Engine |To appear=1 |Year=2024 |Booktitle=Proceedings of the 5th International Workshop on the Resurgence of Datalog in Academia and Industry (Datalog-2.0 2024) |Publisher=CEUR-WS.org |Series=CEUR Workshop Proceedings }} {…“

Datei:Ivliev-Datalog20-2024.pdf

2024-09-13T13:57:02Z

Alex Ivliev: Datalog 2.0 2024 paper about Nemo

Datalog 2.0 2024 paper about Nemo

Inproceedings3392

2024-09-02T09:03:30Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=1
|Year=2024
|Month=Dezember
|Booktitle=Logic Programming and Nonmonotonic Reasoning
|Publisher=Springer
|Editor=Carmine Dodaro, Gopal Gupta, Maria Vanina Martinez
|Series=Lecture Notes in Computer Science
|Volume=15245
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|ISBN=978-3-031-74208-8
|ISSN=0302-9743
|Download=LPNMR2024-Küchenmeister.pdf
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Datei:LPNMR2024-Küchenmeister.pdf

2024-09-02T09:03:26Z

Alex Ivliev: Paper "Towards Mass Spectrum Analysis with ASP"

Paper "Towards Mass Spectrum Analysis with ASP"

Inproceedings3392/en

2024-09-02T09:01:44Z

Alex Ivliev: Page created automatically by parser function on page Inproceedings3392

#REDIRECT [[Inproceedings3392]]

Inproceedings3392

2024-09-02T09:01:44Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Nils |ErsterAutorNachname=Küchenmeister |FurtherAuthors=Alex Ivliev; Markus Krötzsch }} {{Inproceedings |Referiert=0 |Title=Towards Mass Spectrum Analysis with ASP |To appear=1 |Year=2024 |Month=Dezember |Booktitle=Logic Programming and Nonmonotonic Reasoning |Publisher=Springer |Editor=Carmine Dodaro, Gopal Gupta, Maria Vanina Martinez |Series=Lecture Notes in Computer Science |Volume=15245 }} {{Publikatio…“

{{Publikation Erster Autor
|ErsterAutorVorname=Nils
|ErsterAutorNachname=Küchenmeister
|FurtherAuthors=Alex Ivliev; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Towards Mass Spectrum Analysis with ASP
|To appear=1
|Year=2024
|Month=Dezember
|Booktitle=Logic Programming and Nonmonotonic Reasoning
|Publisher=Springer
|Editor=Carmine Dodaro, Gopal Gupta, Maria Vanina Martinez
|Series=Lecture Notes in Computer Science
|Volume=15245
}}
{{Publikation Details
|Abstract=We present a new use of Answer Set Programming (ASP) to discover the molecular structure of chemical samples based on the relative abundance of elements and structural fragments, as measured in mass spectrometry. To constrain the exponential search space for this combinatorial problem, we develop canonical representations of molecular structures and an ASP implementation that uses these definitions. We evaluate the correctness of our implementation over a large set of known molecular structures, and we compare its quality and performance to other ASP symmetry-breaking methods and to a commercial tool from analytical chemistry.
|ISBN=978-3-031-74208-8
|ISSN=0302-9743
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3390

2024-08-16T08:18:01Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Lukas Gerlach; Simon Meusel; Jakob Steinberg; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Nemo: Your Friendly and Versatile Rule Reasoning Toolkit
|To appear=1
|Year=2024
|Booktitle=Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)
|Publisher=International Joint Conferences on Artificial Intelligence Organization
|Series=Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning
|Volume=21
}}
{{Publikation Tool
|Tool=Nemo
}}
{{Publikation Details
|Abstract=We present Nemo, a toolkit for rule-based reasoning and data processing that emphasises robustness and ease of use. Nemo’s core is a scalable and efficient main-memory reasoner that supports an expressive extension of Datalog with support for data types, existential rules, aggregates, and (stratified) negation. Built around this core is a versatile system of libraries and applications for interfacing with several data formats and programming languages, use as a web application, and IDE integration. In this system description, we present this toolkit and discuss relevant application areas in rule-based knowledge representation, knowledge graph processing, and reasoner prototyping. Our evaluation on a range of tasks from these areas demonstrates Nemo’s robust performance in comparison to state-of-the-art rule engines.
|Download=KR-2024-CR.pdf
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3390

2024-08-16T08:17:30Z

Alex Ivliev:

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Lukas Gerlach; Simon Meusel; Jakob Steinberg; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Nemo: Your Friendly and Versatile Rule Reasoning Toolkit
|To appear=1
|Year=2024
|Booktitle=Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)
|Publisher=International Joint Conferences on Artificial Intelligence Organization
|Series=Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning
|Volume=21
}}
{{Publikation Details
|Abstract=We present Nemo, a toolkit for rule-based reasoning and data processing that emphasises robustness and ease of use. Nemo’s core is a scalable and efficient main-memory reasoner that supports an expressive extension of Datalog with support for data types, existential rules, aggregates, and (stratified) negation. Built around this core is a versatile system of libraries and applications for interfacing with several data formats and programming languages, use as a web application, and IDE integration. In this system description, we present this toolkit and discuss relevant application areas in rule-based knowledge representation, knowledge graph processing, and reasoner prototyping. Our evaluation on a range of tasks from these areas demonstrates Nemo’s robust performance in comparison to state-of-the-art rule engines.
|Download=KR-2024-CR.pdf
|Projekt=CPEC, InnoSale, SECAI, ScaDS.AI
|Forschungsgruppe=Wissensbasierte Systeme
}}

Inproceedings3390/en

2024-08-16T08:16:27Z

Alex Ivliev: Page created automatically by parser function on page Inproceedings3390

#REDIRECT [[Inproceedings3390]]

Inproceedings3390

2024-08-16T08:16:27Z

Alex Ivliev: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Alex |ErsterAutorNachname=Ivliev |FurtherAuthors=Lukas Gerlach; Simon Meusel; Jakob Steinberg; Markus Krötzsch }} {{Inproceedings |Referiert=0 |Title=Nemo: Your Friendly and Versatile Rule Reasoning Toolkit |To appear=1 |Year=2024 |Booktitle=Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024) |Publisher=International Joint Conferences on Artifici…“

{{Publikation Erster Autor
|ErsterAutorVorname=Alex
|ErsterAutorNachname=Ivliev
|FurtherAuthors=Lukas Gerlach; Simon Meusel; Jakob Steinberg; Markus Krötzsch
}}
{{Inproceedings
|Referiert=0
|Title=Nemo: Your Friendly and Versatile Rule Reasoning Toolkit
|To appear=1
|Year=2024
|Booktitle=Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024)
|Publisher=International Joint Conferences on Artificial Intelligence Organization
|Series=Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning
|Volume=21
}}
{{Publikation Tool
|Tool=Nemo
}}
{{Publikation Details
|Abstract=We present Nemo, a toolkit for rule-based reasoning and data processing that emphasises robustness and ease of use. Nemo’s core is a scalable and efficient main-memory reasoner that supports an expressive extension of Datalog with support for data types, existential rules, aggregates, and (stratified) negation. Built around this core is a versatile system of libraries and applications for interfacing with several data formats and programming languages, use as a web application, and IDE integration. In this system description, we present this toolkit and discuss relevant application areas in rule-based knowledge representation, knowledge graph processing, and reasoner prototyping. Our evaluation on a range of tasks from these areas demonstrates Nemo’s robust performance in comparison to state-of-the-art rule engines.
|Download=KR-2024-CR.pdf
|Forschungsgruppe=Wissensbasierte Systeme
}}

Datei:KR-2024-CR.pdf

2024-08-16T08:14:22Z

Alex Ivliev: KR paper for Nemo

KR paper for Nemo

Multi-Cultural Commonsense Knowledge Base Construction

2024-08-08T11:08:07Z

Alex Ivliev:

{{Veranstaltung
|Titel EN=Multi-Cultural Commonsense Knowledge Base Construction
|Beschreibung EN=Commonsense knowledge (CSK) about concepts and their properties is useful for AI applications such as robust dialogue. Prior works like ConceptNet, TupleKB and others compiled noteworthy commonsense knowledge bases (CSKBs), but are restricted in their expressiveness to subject-predicate-object (SPO) triples with simple concepts for S and monolithic strings for P and O. Also, these projects have either prioritized precision or recall, but hardly reconcile these complementary goals. In this talk I will present several of our CSKB construction works (DICE, ASCENT, CANDLE, MANGO), where we automatically build large-scale CSKBs with advanced expressiveness and both better precision and recall than prior works.

In DICE, we introduce multi-faceted scoring, and joint reasoning for consistency and corroboration. With ASCENT, we go beyond triples by capturing composite concepts with subgroups and aspects, and by refining assertions with semantic facets. CANDLE focuses on multi-cultural CSK, while MANGO unifies the entity-centric model of ASCENT and the culture-centric model of CANDLE.

The works rely on a combination of textual information extraction and knowledge distillation from LLMs. Intrinsic evaluation shows the superior size and quality of our CSKBs, and extrinsic use cases prove their utility for retrieval-augmented generation.

Links:

Project overview: https://www.mpi-inf.mpg.de/commonsense

Ascent: https://ascent.mpi-inf.mpg.de

Candle: https://candle.mpi-inf.mpg.de

Mango: https://bit.ly/cultural-csk
|Veranstaltungsart=Vortrag
|Start=2024/08/08 11:00:00
|Ende=2024/08/08 12:00:00
|Raum=APB 3027
|Vortragender=Simon Razniewski
|PDF=KBS Seminar 20240808.pdf
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Datei:KBS Seminar 20240808.pdf

2024-08-08T11:07:56Z

Alex Ivliev: Slides for the presentation by Simon Razniewski given in the KBS seminar on the 8th of August 2024.

Slides for the presentation by Simon Razniewski given in the KBS seminar on the 8th of August 2024.