International Center for Computational Logic - Letzte Änderungen [de]

Inproceedings3484

Pascal Kettmann — Tue, 13 Oct 2026 09:41:35 GMT

← Nächstältere Version		Version vom 13. Oktober 2026, 09:41 Uhr
(Eine dazwischenliegende Version desselben Benutzers wird nicht angezeigt)
Zeile 9:		Zeile 9:
	\|To appear=1		\|To appear=1
	\|Year=2026		\|Year=2026
	\|Booktitle=The 10th International Joint Conference on Rules and Reasoning		\|Booktitle=The 10th International Joint Conference on Rules and Reasoning (RuleML+RR 2026)
			\|Publisher=Springer
			\|Series=LNCS
			\|Note=To appear
	}}		}}
	{{Publikation Details		{{Publikation Details
Zeile 15:		Zeile 18:
	In this work, we use the framework of approximating fixpoint theory to formulate well-behaved semantics for fuzzy logic programs containing both “by-failure” and strong negation.		In this work, we use the framework of approximating fixpoint theory to formulate well-behaved semantics for fuzzy logic programs containing both “by-failure” and strong negation.
	We show that this framework generalizes several existing semantics as well as giving rise to a host of new semantics.		We show that this framework generalizes several existing semantics as well as giving rise to a host of new semantics.
			\|Download=Ruleml26-eflp.pdf
	\|Projekt=SECAI		\|Projekt=SECAI
	\|Forschungsgruppe=Computational Logic		\|Forschungsgruppe=Computational Logic
			}}
			{{Forschungsgebiet Auswahl
			\|Forschungsgebiet=Answer Set Programming
			}}
			{{Forschungsgebiet Auswahl
			\|Forschungsgebiet=Nichtmonotones Schließen
	}}		}}

Datei:Ruleml26-eflp.pdf

Pascal Kettmann — Tue, 13 Oct 2026 09:33:42 GMT

Pascal Kettmann lud Datei:Ruleml26-eflp.pdf hoch

Neue Seite

Datei:KG2026-Lecture-01-print.pdf

Markus Krötzsch — Tue, 13 Oct 2026 09:09:30 GMT

Markus Krötzsch lud eine neue Version von Datei:KG2026-Lecture-01-print.pdf hoch

Neue Seite

Datei:KG2026-Lecture-01-overlay.pdf

Markus Krötzsch — Tue, 13 Oct 2026 09:09:21 GMT

Markus Krötzsch lud eine neue Version von Datei:KG2026-Lecture-01-overlay.pdf hoch

Neue Seite

Smallest Synchronizing Terms over Constant Alphabets Can Be Exponentially High

Nils Küchenmeister — Tue, 13 Oct 2026 08:58:47 GMT

Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Smallest Synchronizing Terms over Constant Alphabets Can Be Exponentially High |Veranstaltungsart=Vortrag |Start=2027-01-21 11:00:00 |Ende=2027-01-21 12:00:00 |Raum=APB 3027 |Vortragender=Luisa Herrmann |Forschungsgruppe=Computational Logic |Event series=Research Seminar Logic and AI |In News anzeigen=1 }}“

Neue Seite

{{Veranstaltung
|Titel EN=Smallest Synchronizing Terms over Constant Alphabets Can Be Exponentially High
|Veranstaltungsart=Vortrag
|Start=2027-01-21 11:00:00
|Ende=2027-01-21 12:00:00
|Raum=APB 3027
|Vortragender=Luisa Herrmann
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

A Guided Tour of Sequent Formalisms for Modal Logics

Nils Küchenmeister — Mon, 12 Oct 2026 14:39:47 GMT

Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=A Guided Tour of Sequent Formalisms for Modal Logics |Beschreibung EN=This tutorial explores the landscape of sequent-based proof formalisms for modal logics, using Gödel-Löb provability logic (GL) as a running example. We survey four major paradigms--labeled sequents, nested (or tree) sequents, linear nested sequents, and Gentzen sequents--and discuss the various trade-offs of choosing one formalism over another, including seq…“

Neue Seite

{{Veranstaltung
|Titel EN=A Guided Tour of Sequent Formalisms for Modal Logics
|Beschreibung EN=This tutorial explores the landscape of sequent-based proof formalisms for modal logics, using Gödel-Löb provability logic (GL) as a running example. We survey four major paradigms--labeled sequents, nested (or tree) sequents, linear nested sequents, and Gentzen sequents--and discuss the various trade-offs of choosing one formalism over another, including sequent size, proof size, and suitability for counter-model extraction. The central theme of the tutorial is understanding how these formalisms relate by means of proof transformations, explaining how one can systematically "transition" between them: from graphs, to trees, to lines, and to points (i.e., standard Gentzen sequents). Along the way, we highlight what is lost or gained in each transition, such as invertibility of rules or proof compactness. We also touch on how the choice of formalism affects proof-search algorithms.
|Veranstaltungsart=Vortrag
|Start=2026-12-03 11:00:00
|Ende=2026-12-03 12:00:00
|Raum=APB 3027
|Vortragender=Tim Lyon
|Forschungsgruppe=Computational Logic
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Knowledge Graphs (WS2026)

Markus Krötzsch — Mon, 12 Oct 2026 08:05:15 GMT

← Nächstältere Version		Version vom 12. Oktober 2026, 08:05 Uhr
Zeile 56:		Zeile 56:
	\|Date=2026-10-13		\|Date=2026-10-13
	\|DS=DS3		\|DS=DS3
			\|Download=KG2026-Lecture-01-overlay.pdf, KG2026-Lecture-01-print.pdf
	}}		}}
	{{Vorlesung Zeiten		{{Vorlesung Zeiten

Datei:KG2026-Lecture-01-print.pdf

Markus Krötzsch — Mon, 12 Oct 2026 08:05:11 GMT

Markus Krötzsch lud Datei:KG2026-Lecture-01-print.pdf hoch

Neue Seite

Datei:KG2026-Lecture-01-overlay.pdf

Markus Krötzsch — Mon, 12 Oct 2026 08:05:03 GMT

Markus Krötzsch lud Datei:KG2026-Lecture-01-overlay.pdf hoch

Neue Seite

Knowledge Graphs (WS2026/27)/en

Maximilian Marx — Mon, 12 Oct 2026 07:42:07 GMT

Weiterleitung nach Knowledge Graphs (WS2026)/en erstellt

Neue Seite

#REDIRECT [[Knowledge Graphs (WS2026)/en]]

Knowledge Graphs (WS2026/27)

Maximilian Marx — Mon, 12 Oct 2026 07:41:45 GMT

Weiterleitung nach Knowledge Graphs (WS2026) erstellt

Neue Seite

#REDIRECT [[Knowledge Graphs (WS2026)]]

Complexity Theory (WS2026)

Markus Krötzsch — Mon, 12 Oct 2026 07:21:45 GMT

← Nächstältere Version		Version vom 12. Oktober 2026, 07:21 Uhr
Zeile 73:		Zeile 73:
	\|Date=2026-10-12		\|Date=2026-10-12
	\|DS=DS4		\|DS=DS4
			\|Download=CT2026-Lecture-01-overlay.pdf, CT2026-Lecture-01-print.pdf
	}}		}}
	{{Vorlesung Zeiten		{{Vorlesung Zeiten
Zeile 80:		Zeile 81:
	\|Date=2026-10-13		\|Date=2026-10-13
	\|DS=DS2		\|DS=DS2
			\|Download=CT2026-Lecture-02-overlay.pdf, CT2026-Lecture-02-print.pdf
	}}		}}
	{{Vorlesung Zeiten		{{Vorlesung Zeiten

Datei:CT2026-Lecture-02-print.pdf

Markus Krötzsch — Mon, 12 Oct 2026 07:21:35 GMT

Markus Krötzsch lud Datei:CT2026-Lecture-02-print.pdf hoch

Neue Seite

Datei:CT2026-Lecture-02-overlay.pdf

Markus Krötzsch — Mon, 12 Oct 2026 07:21:27 GMT

Markus Krötzsch lud Datei:CT2026-Lecture-02-overlay.pdf hoch

Neue Seite

Datei:CT2026-Lecture-01-print.pdf

Markus Krötzsch — Mon, 12 Oct 2026 07:21:17 GMT

Markus Krötzsch lud Datei:CT2026-Lecture-01-print.pdf hoch

Neue Seite

Datei:CT2026-Lecture-01-overlay.pdf

Markus Krötzsch — Mon, 12 Oct 2026 07:21:10 GMT

Markus Krötzsch lud Datei:CT2026-Lecture-01-overlay.pdf hoch

Neue Seite

Filippo De Bortoli

Filippo De Bortoli — Sun, 11 Oct 2026 13:49:44 GMT

← Nächstältere Version		Version vom 11. Oktober 2026, 13:49 Uhr
Zeile 5:		Zeile 5:
	\|Forschungsgruppe=Computational Logic		\|Forschungsgruppe=Computational Logic
	\|Stellung=Wissenschaftlicher Mitarbeiter		\|Stellung=Wissenschaftlicher Mitarbeiter
	\|Ehemaliger=0		\|Ehemaliger=1
	\|Email=filippo.de_bortoli@tu-dresden.de		\|Email=filippo.de_bortoli@tu-dresden.de
	\|Matrix=@s5845789:tu-dresden.de		\|Matrix=@s5845789:tu-dresden.de
	~~\|Raum=APB 2031~~
	\|Bild=Filippo-De_Bortoli.jpeg		\|Bild=Filippo-De_Bortoli.jpeg
	\|Info=== Über mich ==		\|Info=== Über mich ==
Zeile 38:		Zeile 37:

	Ich unterstütze die [https://tcs4f.org/ Theoretical Computer Scientists 4 Future]-Initiative.		Ich unterstütze die [https://tcs4f.org/ Theoretical Computer Scientists 4 Future]-Initiative.
	\|Info EN=~~Co-located at S14-717.~~		\|Info EN=== About me ==

	== About me ==

	I have been a research associate at the [[Computational Logic]] group and Coordinator of the [https://scads.ai/education/graduate-school/ Graduate School] at the [[ScaDS.AI\|Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI)]] (of which I am also team member in the [https://scads.ai/transfer/ Transfer and Service] unit) from October 2025 to September 2026.		I have been a research associate at the [[Computational Logic]] group and Coordinator of the [https://scads.ai/education/graduate-school/ Graduate School] at the [[ScaDS.AI\|Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI)]] (of which I am also team member in the [https://scads.ai/transfer/ Transfer and Service] unit) from October 2025 to September 2026.
Zeile 70:		Zeile 67:
	\|DBLP=https://dblp.uni-trier.de/pid/247/4601.html		\|DBLP=https://dblp.uni-trier.de/pid/247/4601.html
	\|Google Scholar=https://scholar.google.com/citations?user=kLIH4Q8AAAAJ&hl=en		\|Google Scholar=https://scholar.google.com/citations?user=kLIH4Q8AAAAJ&hl=en
	~~\|Public Key=0x69C60AF9CE13F663 pub.asc~~
	\|Publikationen anzeigen=1		\|Publikationen anzeigen=1
	\|Abschlussarbeiten anzeigen=0		\|Abschlussarbeiten anzeigen=0

Seminar Knowledge Representation (WS2026)

Sebastian Rudolph — Sun, 11 Oct 2026 09:52:39 GMT

← Nächstältere Version		Version vom 11. Oktober 2026, 09:52 Uhr
(3 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt)
Zeile 5:		Zeile 5:
	\|Term=WS		\|Term=WS
	\|Year=2026		\|Year=2026
	\|Module=INF-25-Ma-FTK-Sem		\|Module=INF-25-Ma-FTK-Sem, CMS-SEM, CMS-SEM-KR
	\|SWSLecture=0		\|SWSLecture=0
	\|SWSExercise=2		\|SWSExercise=2
Zeile 14:		Zeile 14:
	=== Registration ===		=== Registration ===

	To register for ~~this~~ seminar, please ~~complete~~ the poll available [https://bildungsportal.sachsen.de/umfragen/limesurvey/index.php/322922?lang=en under this link] by October 18, 2026. ~~Seminar places~~ for the module ~~INF~~-25-Ma-~~FTK-Sem “Seminar Theoretical Computer Science and Symbolic AI" will be assigned based on the preferences indicated in this form~~.		Seminar places for the module INF-25-Ma-FTK-Sem “Seminar Theoretical Computer Science and Symbolic Artificial Intelligence” will be assigned centrally, based on students’ preferences. To register for our seminar, please indicate your preference in the poll available [https://bildungsportal.sachsen.de/umfragen/limesurvey/index.php/322922?lang=en under this link] by October 18, 2026.

			If you want to take the seminar for the module CMS-SEM “Literature Studies in Computational Modeling,” please send an e-mail to sebastian.rudolph@tu-dresden.de until October 17, 2026.

	=== Prerequisites ===		=== Prerequisites ===
Zeile 32:		Zeile 34:
	'''Diplom Informatik (PO 2025)'''		'''Diplom Informatik (PO 2025)'''
	* {{ModuleLink\|INF-25-Ma-FTK-Sem}}: ''Komplexe Leistung'' (40 hours)		* {{ModuleLink\|INF-25-Ma-FTK-Sem}}: ''Komplexe Leistung'' (40 hours)

			'''Master Computational Modeling and Simulation'''
			* {{ModuleLink\|CMS-SEM}}, {{ModuleLink\|CMS-SEM-KR}}: ''Komplexe Leistung'' (50 hours)

	The ''Komplexe Leistung'' (complex or multi-part examination) consists of a presentation (45 minutes) and an oral question-and-answer session (15 minutes).		The ''Komplexe Leistung'' (complex or multi-part examination) consists of a presentation (45 minutes) and an oral question-and-answer session (15 minutes).
Zeile 37:		Zeile 42:
	=== Contact ===		=== Contact ===

	In case of ~~organizational~~ questions, please send an e-mail to [mailto:sebastian.rudolph@tu-dresden.de sebastian.rudolph@tu-dresden.de].		In case of organisational questions, please send an e-mail to [mailto:sebastian.rudolph@tu-dresden.de sebastian.rudolph@tu-dresden.de].
	\|Title_EN=Seminar “Knowledge Representation”		\|Title_EN=Seminar “Knowledge Representation”
	\|Language=EN		\|Language=EN

Vorlage:ProjektModule2026CL

Sebastian Rudolph — Fri, 09 Oct 2026 18:43:26 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 18:43 Uhr
(2 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt)
Zeile 10:		Zeile 10:
	\|50h		\|50h
	\|-		\|-
	!rowspan="4"\|Master ~~Programm~~		!rowspan="5"\|Master Programme
	\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-BSem.pdf?lang=en INF-25-Ma-BSem]		\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-BSem.pdf?lang=en INF-25-Ma-BSem]
	\|Belegseminar		\|Belegseminar
Zeile 21:		Zeile 21:
	\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-AFT.pdf?lang=en INF-25-Ma-AFT]		\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-AFT.pdf?lang=en INF-25-Ma-AFT]
	\|Analyse eines Forschungsthemas		\|Analyse eines Forschungsthemas
			\|80h
			\|-
			\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-ERS.pdf?lang=en INF-25-Ma-ERS]
			\|Exploration of a Research Subject
	\|80h		\|80h
	\|-		\|-

Projekte und Studienarbeiten Computational Logic

Sebastian Rudolph — Fri, 09 Oct 2026 15:47:50 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 15:47 Uhr
(2 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt)
Zeile 4:		Zeile 4:
	\|Research group=Computational Logic		\|Research group=Computational Logic
	\|Contacts=Sebastian Rudolph		\|Contacts=Sebastian Rudolph
	\|Module=~~MCL-P, INF-PM-FPA, INF-PM-FPG, INF-MA-PR, INF-B-510, INF-B-520, CMS-PRO, CMS-TEA, INF-D-950, INF-D-960,~~ INF-25-Ba-BaSe, INF-25-Ma-FP, INF-25-Ma-BSem, INF-25-Ma-GB, INF-25-Ma-AFT		\|Module=INF-25-Ba-BaSe, INF-25-Ma-FP, INF-25-Ma-BSem, INF-25-Ma-GB, INF-25-Ma-AFT, CMS-VC-TEA
	\|Exam type=Hausarbeit, Referat		\|Exam type=Hausarbeit, Referat
	\|Beschreibung DE==== Neuigkeiten ===		\|Beschreibung DE==== Neuigkeiten ===
Zeile 14:		Zeile 14:
	Zu Beginn eines Semesters sammeln wir neue Themen und stellen diese gebündelt in einem Seminartermin vor. Dieses Seminar bietet Ihnen die Möglichkeit, die neuen Themen und die Betreuer etwas kennenzulernen.		Zu Beginn eines Semesters sammeln wir neue Themen und stellen diese gebündelt in einem Seminartermin vor. Dieses Seminar bietet Ihnen die Möglichkeit, die neuen Themen und die Betreuer etwas kennenzulernen.

	=== Überblick über die Module ~~(Informatikstudiengänge ab PO-Versionen 2025)~~ ===		=== Überblick über die Module ===
	Die Dauer der Bearbeitung von Projekten hängt vom Modul ab. Details über die Anforderungen/Prüfungsmodalitäten werden im Einzelfall mit den jeweiligen Prüfern und Betreunden abgestimmt (bspw. bei komplexen Leistungen/integrated assignments). Die nachfolgende Tabelle liefert lediglich einen ersten Überblick gemäß Modulbeschreibungen.		Die Dauer der Bearbeitung von Projekten hängt vom Modul ab. Details über die Anforderungen/Prüfungsmodalitäten werden im Einzelfall mit den jeweiligen Prüfern und Betreunden abgestimmt (bspw. bei komplexen Leistungen/integrated assignments). Die nachfolgende Tabelle liefert lediglich einen ersten Überblick gemäß Modulbeschreibungen.

Zeile 26:		Zeile 26:
	At the beginning of each semester, we collect new topics and announce them in a seminar-style event. This seminar is an opportunity for you to get to know the new topics and their potential supervisors.		At the beginning of each semester, we collect new topics and announce them in a seminar-style event. This seminar is an opportunity for you to get to know the new topics and their potential supervisors.

	=== Module Overview ~~(from PO versions 2025)~~ ===		=== Module Overview ===
	While the actual project duration depends on the specific module, most of them should be completed ''' within one semester'''.		While the actual project duration depends on the specific module, most of them should be completed ''' within one semester'''.

Vorlage:ProjektModule2026CL

Sebastian Rudolph — Fri, 09 Oct 2026 15:44:03 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 15:44 Uhr
Zeile 26:		Zeile 26:
	\|Forschungsprojekt		\|Forschungsprojekt
	\|200h		\|200h
			\|-
			!rowspan="1"\|CMS Master Programme
			\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/CMS-VC-TEA.pdf?lang=en CMS-VC-TEA]
			\|Team Project
			\|80h
	\|}		\|}

Projekte und Studienarbeiten Computational Logic

Sebastian Rudolph — Fri, 09 Oct 2026 15:36:24 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 15:36 Uhr
Zeile 12:		Zeile 12:
	Neben den Vorlesungen haben Sie während des Studiums die Möglichkeit auch an (Forschungs-)Projekten bei uns zu arbeiten. Auf dieser Seite präsentieren wir Informationen zu den verfügbaren Modulen sowie einzelnen Themen. Die Themen sollen einen Überblick über die Art der Projektthemen, die Sie bei uns bearbeiten können, darstellen. Kontaktieren Sie uns gern, wenn Sie planen, ein Thema bei uns zu bearbeiten. Weitere Themen können wir gern im persönlichen Gespräch durchgehen.		Neben den Vorlesungen haben Sie während des Studiums die Möglichkeit auch an (Forschungs-)Projekten bei uns zu arbeiten. Auf dieser Seite präsentieren wir Informationen zu den verfügbaren Modulen sowie einzelnen Themen. Die Themen sollen einen Überblick über die Art der Projektthemen, die Sie bei uns bearbeiten können, darstellen. Kontaktieren Sie uns gern, wenn Sie planen, ein Thema bei uns zu bearbeiten. Weitere Themen können wir gern im persönlichen Gespräch durchgehen.

	Zu Beginn eines Semesters sammeln wir neue Themen und stellen diese gebündelt in einem Seminartermin vor. Dieses Seminar bietet Ihnen die Möglichkeit, die neuen Themen und die Betreuer etwas kennenzulernen~~. Der genaue Termin wird hier unter '''Termine''' veröffentlicht~~.		Zu Beginn eines Semesters sammeln wir neue Themen und stellen diese gebündelt in einem Seminartermin vor. Dieses Seminar bietet Ihnen die Möglichkeit, die neuen Themen und die Betreuer etwas kennenzulernen.

	=== Überblick über die Module (Informatikstudiengänge ab PO-Versionen 2025) ===		=== Überblick über die Module (Informatikstudiengänge ab PO-Versionen 2025) ===
Zeile 24:		Zeile 24:
	As students, you have several opportunities to do projects with us. Here, we collect information about the different modules and some topics of interest to provide you with an overview of what kind of projects you can do with us. Don't hesitate to get in touch with us if you plan to do one of the modules. We can discuss further topics during a consultation.		As students, you have several opportunities to do projects with us. Here, we collect information about the different modules and some topics of interest to provide you with an overview of what kind of projects you can do with us. Don't hesitate to get in touch with us if you plan to do one of the modules. We can discuss further topics during a consultation.

	At the beginning of each semester, we collect new topics and announce them in a seminar-style event. This seminar is an opportunity for you to get to know the new topics and their potential supervisors~~. The exact date will be published under '''Dates''' on this site~~.		At the beginning of each semester, we collect new topics and announce them in a seminar-style event. This seminar is an opportunity for you to get to know the new topics and their potential supervisors.

	=== Module Overview (from PO versions 2025) ===		=== Module Overview (from PO versions 2025) ===

Vorlage:ProjektModule2026CL

Sebastian Rudolph — Fri, 09 Oct 2026 15:23:45 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 15:23 Uhr
Zeile 5:		Zeile 5:
	!\|Integrated Assignment		!\|Integrated Assignment
	\|-		\|-
	!rowspan="2"\|Bachelor Programme		!rowspan="1"\|Bachelor Programme
	\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ba-BaSe.pdf?lang=en INF-25-Ba-BaSe]		\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ba-BaSe.pdf?lang=en INF-25-Ba-BaSe]
	\|Bachelorseminar		\|Bachelorseminar
	\|50h		\|50h
	\|-
	~~\|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ba-P-KBS.pdf?lang=en INF-25-Ba-P-KBS]~~
	~~\|Knowledge-Based Systems Lab~~
	~~\|80h~~
	\|-		\|-
	!rowspan="4"\|Master Programm		!rowspan="4"\|Master Programm

Projekte und Studienarbeiten Computational Logic

Sebastian Rudolph — Fri, 09 Oct 2026 15:22:56 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 15:22 Uhr
Zeile 17:		Zeile 17:
	Die Dauer der Bearbeitung von Projekten hängt vom Modul ab. Details über die Anforderungen/Prüfungsmodalitäten werden im Einzelfall mit den jeweiligen Prüfern und Betreunden abgestimmt (bspw. bei komplexen Leistungen/integrated assignments). Die nachfolgende Tabelle liefert lediglich einen ersten Überblick gemäß Modulbeschreibungen.		Die Dauer der Bearbeitung von Projekten hängt vom Modul ab. Details über die Anforderungen/Prüfungsmodalitäten werden im Einzelfall mit den jeweiligen Prüfern und Betreunden abgestimmt (bspw. bei komplexen Leistungen/integrated assignments). Die nachfolgende Tabelle liefert lediglich einen ersten Überblick gemäß Modulbeschreibungen.

	{{~~ProjektModule2026~~}}		{{ProjektModule2026CL}}
	\|Beschreibung EN==== News ===		\|Beschreibung EN==== News ===
	* New topics will be presented on '''Thursday, 05 November 2026 at DS5 (2:50 pm) in room [[APB 2026]]'''.		* New topics will be presented on '''Thursday, 05 November 2026 at DS5 (2:50 pm) in room [[APB 2026]]'''.
Zeile 29:		Zeile 29:
	While the actual project duration depends on the specific module, most of them should be completed ''' within one semester'''.		While the actual project duration depends on the specific module, most of them should be completed ''' within one semester'''.

	{{~~ProjektModule2026~~}}		{{ProjektModule2026CL}}
	\|Current=1		\|Current=1
	}}		}}

Vorlage:ProjektModule2026CL

Sebastian Rudolph — Fri, 09 Oct 2026 15:22:20 GMT

Die Seite wurde neu angelegt: „{| class="wikitable" !| !|Modules !|Title !|Integrated Assignment |- !rowspan="2"|Bachelor Programme |[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ba-BaSe.pdf?lang=en INF-25-Ba-BaSe] |Bachelorseminar |50h |- |[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ba-P-KBS.pdf?lang=en INF-25-Ba-P-KBS] |Knowledge-Based Systems Lab |80h |- !rowspan="4"|Mas…“

Neue Seite

{| class="wikitable"
!|
!|Modules
!|Title
!|Integrated Assignment
|-
!rowspan="2"|Bachelor Programme
|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ba-BaSe.pdf?lang=en INF-25-Ba-BaSe]
|Bachelorseminar
|50h
|-
|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ba-P-KBS.pdf?lang=en INF-25-Ba-P-KBS]
|Knowledge-Based Systems Lab
|80h
|-
!rowspan="4"|Master Programm
|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-BSem.pdf?lang=en INF-25-Ma-BSem]
|Belegseminar
|50h
|-
|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-GB.pdf?lang=en INF-25-Ma-GB]
|Großer Beleg
|180h
|-
|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-AFT.pdf?lang=en INF-25-Ma-AFT]
|Analyse eines Forschungsthemas
|80h
|-
|[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-25/de/INF-25-Ma-FP.pdf?lang=en INF-25-Ma-FP]
|Forschungsprojekt
|200h
|}

Projekte und Studienarbeiten Computational Logic

Sebastian Rudolph — Fri, 09 Oct 2026 15:20:42 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 15:20 Uhr
Zeile 6:		Zeile 6:
	\|Module=MCL-P, INF-PM-FPA, INF-PM-FPG, INF-MA-PR, INF-B-510, INF-B-520, CMS-PRO, CMS-TEA, INF-D-950, INF-D-960, INF-25-Ba-BaSe, INF-25-Ma-FP, INF-25-Ma-BSem, INF-25-Ma-GB, INF-25-Ma-AFT		\|Module=MCL-P, INF-PM-FPA, INF-PM-FPG, INF-MA-PR, INF-B-510, INF-B-520, CMS-PRO, CMS-TEA, INF-D-950, INF-D-960, INF-25-Ba-BaSe, INF-25-Ma-FP, INF-25-Ma-BSem, INF-25-Ma-GB, INF-25-Ma-AFT
	\|Exam type=Hausarbeit, Referat		\|Exam type=Hausarbeit, Referat
	\|Beschreibung DE=~~Auf dieser Seite präsentieren wir Informationen zu~~ den ~~verfügbaren Modulen im Rahmen derer an der Professur Computational Logic studentische Projekte bearbeitet werden können~~. ~~Kontaktieren Sie uns gern, wenn Sie Interesse daran haben, ein Thema bei uns zu bearbeiten~~.		\|Beschreibung DE==== Neuigkeiten ===
			* Die nächste Themenvorstellung findet am '''Donnerstag, den 05. November 2026 DS5 (um 14:50 Uhr) in Raum [[APB 2026]]''' statt.

	~~Die Dauer der Bearbeitung von~~ Projekten ~~hängt vom Modul ab~~. In der ~~Regel sind diese '''innerhalb eines Semesters''' zu~~ bearbeiten, ~~mit der Ausnahme des Moduls [https://tu-dresden~~.~~de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-ma-pr~~.~~pdf?lang=en INF-MA-PR], welches '''innerhalb von zwei Semestern''' absolviert wird~~.		=== Themensammlung und Themenvergabe ===
			Neben den Vorlesungen haben Sie während des Studiums die Möglichkeit auch an (Forschungs-)Projekten bei uns zu arbeiten. Auf dieser Seite präsentieren wir Informationen zu den verfügbaren Modulen sowie einzelnen Themen. Die Themen sollen einen Überblick über die Art der Projektthemen, die Sie bei uns bearbeiten können, darstellen. Kontaktieren Sie uns gern, wenn Sie planen, ein Thema bei uns zu bearbeiten. Weitere Themen können wir gern im persönlichen Gespräch durchgehen.

	~~Einige Module ([https://tu-dresden~~.~~de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-pm-fpa.pdf?lang=en INF-PM-FPA]~~, ~~[https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-pm-fpg~~.~~pdf?lang=en INF-PM-FPG]) bieten sich auch als~~ '''~~vorbereitende Studien für Ihre Master- oder Diplomarbeit~~''' an.		Zu Beginn eines Semesters sammeln wir neue Themen und stellen diese gebündelt in einem Seminartermin vor. Dieses Seminar bietet Ihnen die Möglichkeit, die neuen Themen und die Betreuer etwas kennenzulernen. Der genaue Termin wird hier unter '''Termine''' veröffentlicht.

	~~{{ProjektModuleCL}}~~		=== Überblick über die Module (Informatikstudiengänge ab PO-Versionen 2025) ===
	~~\|Beschreibung EN=At this page you find information regarding different modules in the course of which you can do projects at the chair of Computational Logic~~. ~~Please contact us if are interested in one of the modules~~.		Die Dauer der Bearbeitung von Projekten hängt vom Modul ab. Details über die Anforderungen/Prüfungsmodalitäten werden im Einzelfall mit den jeweiligen Prüfern und Betreunden abgestimmt (bspw. bei komplexen Leistungen/integrated assignments). Die nachfolgende Tabelle liefert lediglich einen ersten Überblick gemäß Modulbeschreibungen.

	~~The actual project duration depends~~ on ~~the specific module. Most of them should be completed~~ '''~~within one semester''' with the exception of~~ [~~https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-ma-pr.pdf?lang=en INF-MA-PR~~] ~~which has a '''duration of two semesters~~'''.		{{ProjektModule2026}}
			\|Beschreibung EN==== News ===
			* New topics will be presented on '''Thursday, 05 November 2026 at DS5 (2:50 pm) in room [[APB 2026]]'''.

	~~Some of the modules ([https://tu-dresden.de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-pm-fpa.pdf?lang~~=~~en INF-PM-FPA]~~, ~~[https://tu-dresden~~.~~de/ing/informatik/ressourcen/dateien/studium/modulbeschreibungen/inf-pm-fpg.pdf?lang=en INF-PM-FPG]) provide~~ the ~~opportunity~~ to '~~''prepare for your Master or Diploma thesis'''~~.		=== Topics ===
			As students, you have several opportunities to do projects with us. Here, we collect information about the different modules and some topics of interest to provide you with an overview of what kind of projects you can do with us. Don't hesitate to get in touch with us if you plan to do one of the modules. We can discuss further topics during a consultation.

	{{~~ProjektModuleCL~~}}		At the beginning of each semester, we collect new topics and announce them in a seminar-style event. This seminar is an opportunity for you to get to know the new topics and their potential supervisors. The exact date will be published under '''Dates''' on this site.

			=== Module Overview (from PO versions 2025) ===
			While the actual project duration depends on the specific module, most of them should be completed ''' within one semester'''.

			{{ProjektModule2026}}
	\|Current=1		\|Current=1
	}}		}}

Reinforcement Learning for BDD Variable Ordering

Nils Küchenmeister — Fri, 09 Oct 2026 08:39:47 GMT

← Nächstältere Version		Version vom 9. Oktober 2026, 08:39 Uhr
Zeile 1:		Zeile 1:
	{{Veranstaltung		{{Veranstaltung
	\|Titel EN=Reinforcement Learning ~~for~~ BDD ~~Variable Ordering~~		\|Titel EN=Learning to Control Binary Decision Diagrams with Reinforcement Learning
			\|Beschreibung EN=Binary Decision Diagrams (BDDs) are a powerful representation of Boolean functions, supporting efficient logical operations and reasoning over large state spaces. However, their practical effectiveness depends heavily on the ordering of variables, with poor orderings potentially causing an exponential increase in representation size. A major limitation of standard BDD-based computation is its reliance on computationally expensive dynamic variable reordering heuristics, which perform extensive search to optimise the size of a static set of diagrams. These methods are fundamentally reactive, aiming to repair variable orderings once the diagrams have already grown substantially large, rather than preventing this growth in the first place. In this talk, I will present my ongoing PhD research on developing a reinforcement learning controller that continuously regulates variable ordering throughout BDD construction and manipulation. Rather than relying on expensive search to repair large diagrams, the objective is to learn a predictive reordering policy that makes decisions directly from the structure of the current diagrams, proactively maintaining compact representations as computation progresses.
	\|Veranstaltungsart=Vortrag		\|Veranstaltungsart=Vortrag
	\|Start=2026-11-05 11:00:00		\|Start=2026-11-05 11:00:00

Inproceedings3484

Pascal Kettmann — Thu, 08 Oct 2026 11:52:47 GMT

← Nächstältere Version		Version vom 8. Oktober 2026, 11:52 Uhr
Zeile 12:		Zeile 12:
	}}		}}
	{{Publikation Details		{{Publikation Details
			\|Abstract=In logic programming, negation can be interpreted in various ways. Probably best known is the concept of “negation as failure”, where “not p” is true if we have no evidence for p. On the other hand, strong negation requires that we have evidence for p being false. Defining semantics for logic programs containing both kinds of negation is a challenging task, and this becomes even more challenging when combining this with other extensions of logic programming, e.g. fuzziness.
			In this work, we use the framework of approximating fixpoint theory to formulate well-behaved semantics for fuzzy logic programs containing both “by-failure” and strong negation.
			We show that this framework generalizes several existing semantics as well as giving rise to a host of new semantics.
	\|Projekt=SECAI		\|Projekt=SECAI
	\|Forschungsgruppe=Computational Logic		\|Forschungsgruppe=Computational Logic
	}}		}}

Inproceedings3484

Pascal Kettmann — Thu, 08 Oct 2026 11:44:50 GMT

Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Pascal |ErsterAutorNachname=Kettmann |FurtherAuthors=Hannes Straß; Jesse Heyninck; Jeroen Spaans }} {{Inproceedings |Referiert=1 |Title=Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory |To appear=1 |Year=2026 |Booktitle=The 10th International Joint Conference on Rules and Reasoning }} {{Publikation Details |Projekt=SECAI |Forschungsgruppe=Computational Logic }}“

Neue Seite

{{Publikation Erster Autor
|ErsterAutorVorname=Pascal
|ErsterAutorNachname=Kettmann
|FurtherAuthors=Hannes Straß; Jesse Heyninck; Jeroen Spaans
}}
{{Inproceedings
|Referiert=1
|Title=Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory
|To appear=1
|Year=2026
|Booktitle=The 10th International Joint Conference on Rules and Reasoning
}}
{{Publikation Details
|Projekt=SECAI
|Forschungsgruppe=Computational Logic
}}

Datei:Eflp-aft-ruleml26.pdf

Pascal Kettmann — Thu, 08 Oct 2026 11:37:45 GMT

Pascal Kettmann lud Datei:Eflp-aft-ruleml26.pdf hoch

Neue Seite

Datei:Foto francesco.jpg

Francesco Kriegel — Thu, 08 Oct 2026 10:58:52 GMT

Francesco Kriegel löschte die Seite Datei:Foto francesco.jpg Inhalt war: „“. Einziger Bearbeiter: Francesco Kriegel (Diskussion)

Reinforcement Learning for BDD Variable Ordering

Nils Küchenmeister — Thu, 08 Oct 2026 10:29:47 GMT

Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Reinforcement Learning for BDD Variable Ordering |Veranstaltungsart=Vortrag |Start=2026-11-05 11:00:00 |Ende=2026-11-05 12:00:00 |Raum=APB 3027 |Vortragender=Luke Slater |Eingeladen durch=Markus Krötzsch |Forschungsgruppe=Wissensbasierte Systeme |Event series=Research Seminar Logic and AI |In News anzeigen=1 }}“

Neue Seite

{{Veranstaltung
|Titel EN=Reinforcement Learning for BDD Variable Ordering
|Veranstaltungsart=Vortrag
|Start=2026-11-05 11:00:00
|Ende=2026-11-05 12:00:00
|Raum=APB 3027
|Vortragender=Luke Slater
|Eingeladen durch=Markus Krötzsch
|Forschungsgruppe=Wissensbasierte Systeme
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Survey of Syntax Splitting

Nils Küchenmeister — Thu, 08 Oct 2026 10:25:57 GMT

Die Seite wurde neu angelegt: „{{Veranstaltung |Titel EN=Survey of Syntax Splitting |Veranstaltungsart=Vortrag |Start=2026-11-12 11:00:00 |Ende=2026-11-12 12:00:00 |Raum=APB 3027 |Vortragender=Ameerah Allie |Eingeladen durch=Markus Krötzsch |Forschungsgruppe=Wissensbasierte Systeme |Event series=Research Seminar Logic and AI |In News anzeigen=1 }}“

Neue Seite

{{Veranstaltung
|Titel EN=Survey of Syntax Splitting
|Veranstaltungsart=Vortrag
|Start=2026-11-12 11:00:00
|Ende=2026-11-12 12:00:00
|Raum=APB 3027
|Vortragender=Ameerah Allie
|Eingeladen durch=Markus Krötzsch
|Forschungsgruppe=Wissensbasierte Systeme
|Event series=Research Seminar Logic and AI
|In News anzeigen=1
}}

Advanced Problem Solving and Search (WS2026)

Sarah Gaggl — Thu, 08 Oct 2026 08:29:11 GMT

← Nächstältere Version		Version vom 8. Oktober 2026, 08:29 Uhr
Zeile 110:		Zeile 110:
	\|Lehrveranstaltungstype=Übung		\|Lehrveranstaltungstype=Übung
	\|Title=Tutorial Gr2-Fr 1 (Traditional Search)		\|Title=Tutorial Gr2-Fr 1 (Traditional Search)
	\|Room=APB ~~E008~~		\|Room=APB E006
	\|Date=2026-10-30		\|Date=2026-10-30
	\|DS=DS4		\|DS=DS4
	}}		}}

Inproceedings3473

Hannes Straß — Wed, 07 Oct 2026 09:11:05 GMT

← Nächstältere Version		Version vom 7. Oktober 2026, 09:11 Uhr
Zeile 7:		Zeile 7:
	\|Referiert=1		\|Referiert=1
	\|Title=Assumption-Based Argumentation Through the Lens of Approximation Fixpoint Theory		\|Title=Assumption-Based Argumentation Through the Lens of Approximation Fixpoint Theory
	\|To appear=1		\|To appear=0
	\|Year=2026		\|Year=2026
	\|Booktitle=Proceedings of the Eleventh International Conference on Computational Models of Argument (COMMA)		\|Booktitle=Proceedings of the Eleventh International Conference on Computational Models of Argument (COMMA)
			\|Pages=437–448
	\|Publisher=IOS Press		\|Publisher=IOS Press
	\|Editor=Katie Atkinson		\|Editor=Katie Atkinson

Inproceedings3472

Hannes Straß — Wed, 07 Oct 2026 09:10:28 GMT

← Nächstältere Version		Version vom 7. Oktober 2026, 09:10 Uhr
Zeile 7:		Zeile 7:
	\|Referiert=1		\|Referiert=1
	\|Title=On the Complexity of Initial Models in Abstract Dialectical Frameworks		\|Title=On the Complexity of Initial Models in Abstract Dialectical Frameworks
	\|To appear=1		\|To appear=0
	\|Year=2026		\|Year=2026
	\|Booktitle=Proceedings of the Eleventh International Conference on Computational Models of Argument (COMMA)		\|Booktitle=Proceedings of the Eleventh International Conference on Computational Models of Argument (COMMA)
			\|Pages=113–124
	\|Publisher=IOS Press		\|Publisher=IOS Press
	\|Editor=Katie Atkinson		\|Editor=Katie Atkinson

Research Seminar Logic and AI

Nils Küchenmeister — Wed, 07 Oct 2026 08:12:39 GMT

← Nächstältere Version		Version vom 7. Oktober 2026, 08:12 Uhr
Zeile 27:		Zeile 27:
	===Schedule and Location===		===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] (''~~to be updated~~'') and physically in the room [[APB 3027/en\|APB 3027]].		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/j5s-hql-zmm-mgz/join Big Blue Button] (''This is a new link!'') and physically in the room [[APB 3027/en\|APB 3027]].

	For further information on scheduled upcoming seminars please check the program overview below.		For further information on scheduled upcoming seminars please check the program overview below.

Inproceedings3483

Tim Lyon — Wed, 07 Oct 2026 07:35:32 GMT

Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Tim |ErsterAutorNachname=Lyon |FurtherAuthors=Omar Taher }} {{Inproceedings |Referiert=1 |Title=Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents |To appear=0 |Year=2026 |Booktitle=Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2026) |Pages=148-164 |Publisher=Electronic Proceedings in Theoretical Computer Scien…“

Neue Seite

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
|FurtherAuthors=Omar Taher
}}
{{Inproceedings
|Referiert=1
|Title=Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
|To appear=0
|Year=2026
|Booktitle=Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2026)
|Pages=148-164
|Publisher=Electronic Proceedings in Theoretical Computer Science
|Editor=Giorgio Bacci and Mickaël Randour
|Volume=454
}}
{{Publikation Details
|Abstract=We answer a question posed by Poggiolesi concerning a syntactic decidability proof for GL in the tree-hypersequent system CSGL, and resolve a challenge identified by Maggesi and Perini Brogi, who sought a PSPACE proof-search algorithm for GL in expressive sequent-based formalisms. We work with a notational variant of CSGL formulated in terms of (labeled) tree sequents. Our answer is complexity-optimal: we present a proof-search algorithm that decides the (in)validity of formulae and runs in PSPACE, matching the known PSPACE-completeness of GL. To achieve this, we introduce a "linearization method", which constructs only a single branch of a derivation and of a tree sequent at a time, avoiding the exponential blowup typical of naive proof-search in sequent formalisms. We show how to systematically combine fragments of tree sequents generated during proof-search to extract finite counter-models, which serves as a theoretical device for establishing the correctness of the algorithm when proof-search fails. Finally, we show that every valid formula admits a proof consisting solely of line sequents, which correspond to linear nested sequents. This establishes a connection between depth-first proof-search and linear nested sequent calculi. Our results not only answer the aforementioned questions, but also provide new insights into proof-search and correctness arguments in tree sequent systems for modal logics.
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Inproceedings3482

Tim Lyon — Wed, 07 Oct 2026 07:33:28 GMT

Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Tim |ErsterAutorNachname=Lyon |FurtherAuthors=Lukas Zenger }} {{Inproceedings |Referiert=1 |Title=Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents |To appear=0 |Year=2026 |Booktitle=Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2026) |Pages=165-182 |Publisher=Electronic Proceedings in Theoretical Co…“

Neue Seite

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
|FurtherAuthors=Lukas Zenger
}}
{{Inproceedings
|Referiert=1
|Title=Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
|To appear=0
|Year=2026
|Booktitle=Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2026)
|Pages=165-182
|Publisher=Electronic Proceedings in Theoretical Computer Science
|Editor=Giorgio Bacci and Mickaël Randour
|Volume=454
}}
{{Publikation Details
|Abstract=We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear temporal logic (LTL). The paper addresses two central problems, which we call "cycle recognition" and "unraveling." Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call "saturation recurrence," which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}