https://iccl.inf.tu-dresden.de/w/api.php?action=feedcontributions&feedformat=atom&user=Tim+Lyon 2026-10-06T16:32:38Z Benutzerbeiträge MediaWiki 1.43.1 https://iccl.inf.tu-dresden.de/w/index.php?title=Techreport3063&diff=45129 2026-10-05T12:53:06Z

<p>Tim Lyon: </p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Lukas Zenger<br /> }}<br /> {{Techreport<br /> |Title=Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents<br /> |Year=2026<br /> |Institution=TU Dresden<br /> |Note=full version; accepted to Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2026)<br /> }}<br /> {{Publikation Details<br /> |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 &quot;cycle recognition&quot; and &quot;unraveling.&quot; 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 &quot;saturation recurrence,&quot; 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.<br /> |Download=GandALF26 Full LyoZen.pdf<br /> |Forschungsgruppe=Computational Logic<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Modal- und Temporallogiken<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:GandALF26_Full_LyoZen.pdf&diff=45128 2026-10-05T12:53:03Z

<p>Tim Lyon: Full version of &quot;Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents&quot; (published at GandALF 2026)</p> <hr /> <div>Full version of &quot;Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents&quot; (published at GandALF 2026)</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Article3123&diff=45106 2026-10-03T13:57:54Z

<p>Tim Lyon: </p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Piotr Ostropolski-Nalewaja<br /> }}<br /> {{Article<br /> |Referiert=1<br /> |Title=Foundations for an Abstract Proof Theory in the Context of Horn Rules<br /> |To appear=0<br /> |Year=2026<br /> |Month=Oktober<br /> |Journal=ACM Transactions on Computational Logic<br /> |Volume=27<br /> |Number=4<br /> |Publisher=Association for Computing Machinery<br /> }}<br /> {{Publikation Details<br /> |Abstract=We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed &quot;g-sequents,&quot; which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of inference rule types as sets of operations that act over such objects, and define abstract (sequent) calculi as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any multisequent proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.<br /> |DOI Name=10.1145/3821208<br /> |Projekt=DeciGUT<br /> |Forschungsgruppe=Computational Logic<br /> |BibTex=@article{10.1145/3821208,<br /> author = {Lyon, Tim S. and Ostropolski-Nalewaja, Piotr},<br /> title = {Foundations for an Abstract Proof Theory in the Context of Horn Rules},<br /> year = {2026},<br /> issue_date = {October 2026},<br /> publisher = {Association for Computing Machinery},<br /> address = {New York, NY, USA},<br /> volume = {27},<br /> number = {4},<br /> issn = {1529-3785},<br /> url = {https://doi.org/10.1145/3821208},<br /> doi = {10.1145/3821208},<br /> abstract = {We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed g-sequents, which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of inference rule types as sets of operations that act over such objects, and define abstract (sequent) calculi as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any multisequent proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.},<br /> journal = {ACM Trans. Comput. Logic},<br /> month = aug,<br /> articleno = {25},<br /> numpages = {42},<br /> keywords = {Calculus, Constraint, Graph, Horn property, Labeled sequent, Lattice, Nested sequent, Permutation, Polytree, Proof theory, Proof transformation, Sequent, Simulation, Structural refinement}<br /> }<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Article3123&diff=45105 2026-10-03T13:57:26Z

<p>Tim Lyon: </p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Piotr Ostropolski-Nalewaja<br /> }}<br /> {{Article<br /> |Referiert=1<br /> |Title=Foundations for an Abstract Proof Theory in the Context of Horn Rules<br /> |To appear=0<br /> |Year=2026<br /> |Month=Juni<br /> |Journal=ACM Transactions on Computational Logic<br /> |Volume=27<br /> |Number=4<br /> |Publisher=Association for Computing Machinery<br /> }}<br /> {{Publikation Details<br /> |Abstract=We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed &quot;g-sequents,&quot; which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of inference rule types as sets of operations that act over such objects, and define abstract (sequent) calculi as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any multisequent proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.<br /> |DOI Name=10.1145/3821208<br /> |Projekt=DeciGUT<br /> |Forschungsgruppe=Computational Logic<br /> |BibTex=@article{10.1145/3821208,<br /> author = {Lyon, Tim S. and Ostropolski-Nalewaja, Piotr},<br /> title = {Foundations for an Abstract Proof Theory in the Context of Horn Rules},<br /> year = {2026},<br /> issue_date = {October 2026},<br /> publisher = {Association for Computing Machinery},<br /> address = {New York, NY, USA},<br /> volume = {27},<br /> number = {4},<br /> issn = {1529-3785},<br /> url = {https://doi.org/10.1145/3821208},<br /> doi = {10.1145/3821208},<br /> abstract = {We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed g-sequents, which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of inference rule types as sets of operations that act over such objects, and define abstract (sequent) calculi as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any multisequent proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.},<br /> journal = {ACM Trans. Comput. Logic},<br /> month = aug,<br /> articleno = {25},<br /> numpages = {42},<br /> keywords = {Calculus, Constraint, Graph, Horn property, Labeled sequent, Lattice, Nested sequent, Permutation, Polytree, Proof theory, Proof transformation, Sequent, Simulation, Structural refinement}<br /> }<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News114&diff=45063 2026-09-23T10:14:38Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß und Pascal Kettmann gewinnen den Harold Boley Distinguished Paper Award<br /> |Titel EN=Hannes Straß and Pascal Kettmann win the Harold Boley Distinguished Paper Award<br /> |Beschreibung DE=&lt;p&gt;Die Computational Logic Group freut sich, bekannt zu geben, dass die Arbeit „Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory“ von Pascal Kettmann, Hannes Straß, Jesse Heyninck und Jeroen Spaans den Harold Boley Distinguished Paper Award auf der 10. Internationalen Gemeinsamen Konferenz über Regeln und Schlussfolgerungen (RuleML+RR 2026) erhalten hat .&lt;/p&gt;<br /> <br /> Die Arbeit liefert ein einheitliches Rahmenwerk für erweiterte Fuzzy‑Logik‑Programme, indem sie fuzzy‑logisches Schließen mit Negation durch Fehlschlag und starker Negation mittels Approximation Fixpoint Theory (AFT) verbindet. Damit werden u. a. die Stable‑Model‑ und Well‑Founded‑Semantik abgedeckt.<br /> <br /> Eine erweiterte Version ist auf arXiv verfügbar: [https://arxiv.org/abs/2605.05286 Extended Version]<br /> |Beschreibung EN=&lt;p&gt;The Computational Logic Group is delighted to announce that the paper “Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory” by Pascal Kettmann, Hannes Straß, Jesse Heyninck, and Jeroen Spaans has received the Harold Boley Distinguished Paper Award at the 10th International Joint Conference on Rules and Reasoning (RuleML+RR 2026) .&lt;/p&gt;<br /> <br /> <br /> The contribution develops a unified semantics for extended fuzzy logic programs by combining fuzzy reasoning with two forms of negation—negation as failure and strong negation—through Approximation Fixpoint Theory (AFT). This framework subsumes several well‑known semantics, including stable‑model and well‑founded semantics.<br /> <br /> An extended version of the paper can be accessed on arXiv: [https://arxiv.org/abs/2605.05286 Extended Version]<br /> |Datum=2026-09-23<br /> |Bild=Best paper award.jpg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News114&diff=45062 2026-09-23T10:13:40Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß und Pascal Kettmann gewinnen den Harold Boley Distinguished Paper Award<br /> |Titel EN=Hannes Straß and Pascal Kettmann win the Harold Boley Distinguished Paper Award<br /> |Beschreibung DE=&lt;p&gt;Die Computational Logic Group freut sich, bekannt zu geben, dass die Arbeit „Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory“ von Pascal Kettmann, Hannes Straß, Jesse Heyninck und Jeroen Spaans den Harold Boley Distinguished Paper Award auf der 10. Internationalen Gemeinsamen Konferenz über Regeln und Schlussfolgerungen (RuleML+RR 2026) erhalten hat .&lt;/p&gt;<br /> <br /> Die Arbeit liefert ein einheitliches Rahmenwerk für erweiterte Fuzzy‑Logik‑Programme, indem sie fuzzy‑logisches Schließen mit Negation durch Fehlschlag und starker Negation mittels Approximation Fixpoint Theory (AFT) verbindet. Damit werden u. a. die Stable‑Model‑ und Well‑Founded‑Semantik abgedeckt.<br /> <br /> Eine erweiterte Version ist auf arXiv verfügbar: [https://arxiv.org/abs/2605.05286 Preprint]<br /> |Beschreibung EN=&lt;p&gt;The Computational Logic Group is delighted to announce that the paper “Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory” by Pascal Kettmann, Hannes Straß, Jesse Heyninck, and Jeroen Spaans has received the Harold Boley Distinguished Paper Award at the 10th International Joint Conference on Rules and Reasoning (RuleML+RR 2026) .&lt;/p&gt;<br /> <br /> <br /> The contribution develops a unified semantics for extended fuzzy logic programs by combining fuzzy reasoning with two forms of negation—negation as failure and strong negation—through Approximation Fixpoint Theory (AFT). This framework subsumes several well‑known semantics, including stable‑model and well‑founded semantics.<br /> <br /> An extended version of the paper can be accessed on arXiv: [https://arxiv.org/abs/2605.05286 Preprint]<br /> |Datum=2026-09-23<br /> |Bild=Best paper award.jpg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News114&diff=45061 2026-09-23T10:10:33Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß und Pascal Kettmann gewinnen den Harold Boley Distinguished Paper Award<br /> |Titel EN=Hannes Straß and Pascal Kettmann win the Harold Boley Distinguished Paper Award<br /> |Beschreibung DE=Die Computational Logic Group freut sich, bekannt zu geben, dass die Arbeit „Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory“ von Pascal Kettmann, Hannes Straß, Jesse Heyninck und Jeroen Spaans den Harold Boley Distinguished Paper Award auf der 10. Internationalen Gemeinsamen Konferenz über Regeln und Schlussfolgerungen (RuleML+RR 2026) erhalten hat . <br /> <br /> Die Arbeit liefert ein einheitliches Rahmenwerk für erweiterte Fuzzy‑Logik‑Programme, indem sie fuzzy‑logisches Schließen mit Negation durch Fehlschlag und starker Negation mittels Approximation Fixpoint Theory (AFT) verbindet. Damit werden u. a. die Stable‑Model‑ und Well‑Founded‑Semantik abgedeckt.<br /> |Beschreibung EN=The Computational Logic Group is delighted to announce that the paper “Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory” by Pascal Kettmann, Hannes Straß, Jesse Heyninck, and Jeroen Spaans has received the Harold Boley Distinguished Paper Award at the 10th International Joint Conference on Rules and Reasoning (RuleML+RR 2026) . <br /> <br /> The contribution develops a unified semantics for extended fuzzy logic programs by combining fuzzy reasoning with two forms of negation—negation as failure and strong negation—through Approximation Fixpoint Theory (AFT). This framework subsumes several well‑known semantics, including stable‑model and well‑founded semantics.<br /> |Link PDF=https://arxiv.org/abs/2605.05286<br /> |Datum=2026-09-23<br /> |Bild=Best paper award.jpg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News114&diff=45059 2026-09-23T10:10:08Z

<p>Tim Lyon: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Hannes Straß und Pascal Kettmann gewinnen den Harold Boley Distinguished Paper Award |Titel EN=Hannes Straß and Pascal Kettmann win the Harold Boley Distinguished Paper Award |Beschreibung DE=Die Computational Logic Group freut sich, bekannt zu geben, dass die Arbeit „Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory“ von Pascal Kettmann, Hannes Straß, Jesse Heyninck und J…“</p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß und Pascal Kettmann gewinnen den Harold Boley Distinguished Paper Award<br /> |Titel EN=Hannes Straß and Pascal Kettmann win the Harold Boley Distinguished Paper Award<br /> |Beschreibung DE=Die Computational Logic Group freut sich, bekannt zu geben, dass die Arbeit „Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory“ von Pascal Kettmann, Hannes Straß, Jesse Heyninck und Jeroen Spaans den Harold Boley Distinguished Paper Award auf der 10. Internationalen Gemeinsamen Konferenz über Regeln und Schlussfolgerungen (RuleML+RR 2026) erhalten hat .<br /> <br /> Die Arbeit liefert ein einheitliches Rahmenwerk für erweiterte Fuzzy‑Logik‑Programme, indem sie fuzzy‑logisches Schließen mit Negation durch Fehlschlag und starker Negation mittels Approximation Fixpoint Theory (AFT) verbindet. Damit werden u. a. die Stable‑Model‑ und Well‑Founded‑Semantik abgedeckt.<br /> |Beschreibung EN=The Computational Logic Group is delighted to announce that the paper “Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory” by Pascal Kettmann, Hannes Straß, Jesse Heyninck, and Jeroen Spaans has received the Harold Boley Distinguished Paper Award at the 10th International Joint Conference on Rules and Reasoning (RuleML+RR 2026) .<br /> <br /> The contribution develops a unified semantics for extended fuzzy logic programs by combining fuzzy reasoning with two forms of negation—negation as failure and strong negation—through Approximation Fixpoint Theory (AFT). This framework subsumes several well‑known semantics, including stable‑model and well‑founded semantics.<br /> |URL=https://arxiv.org/abs/2605.05286<br /> |Datum=2026-09-23<br /> |Bild=Best paper award.jpg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:Best_paper_award.jpg&diff=45058 2026-09-23T10:09:58Z

<p>Tim Lyon: Pascal and Hannes Award 2026</p> <hr /> <div>Pascal and Hannes Award 2026</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(WS2026)&diff=45057 2026-09-23T08:07:38Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=WS<br /> |Year=2026<br /> |Module=INF-25-MA-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 9:20 – 10:50 in room APB E007. The first class will take place on 16 October 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E007<br /> |Date=2026-10-16<br /> |DS=DS2<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(WS2026)&diff=45056 2026-09-23T08:05:16Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=WS<br /> |Year=2026<br /> |Module=INF-25-MA-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 9:20 – 10:50 in room APB E007.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E007<br /> |Date=2026-10-16<br /> |DS=DS2<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(WS2026)&diff=45054 2026-09-23T08:00:16Z

<p>Tim Lyon: Die Seite wurde neu angelegt: „{{Vorlesung |Title=Proof Theory and Sequent Systems |Research group=Computational Logic |Lecturers=Tim Lyon |Term=WS |Year=2026 |Module=INF-25-MA-FTK-ASAI, INF-BAS2, INF-VERT2 |SWSLecture=2 |SWSExercise=0 |SWSPractical=0 |Exam type=mündliche Prüfung |Description====Course Description=== Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as synt…“</p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=WS<br /> |Year=2026<br /> |Module=INF-25-MA-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 9:20 – 10:50 in room APB E007.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Techreport3063&diff=44974 2026-09-11T13:28:42Z

<p>Tim Lyon: </p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Lukas Zenger<br /> }}<br /> {{Techreport<br /> |Title=Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents<br /> |Year=2026<br /> |Institution=TU Dresden<br /> |Note=Full, Appended Version. Accepted to GandALF 2026.<br /> }}<br /> {{Publikation Details<br /> |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 &quot;cycle recognition&quot; and &quot;unraveling.&quot; 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 &quot;saturation recurrence,&quot; 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.<br /> |Forschungsgruppe=Computational Logic<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Modal- und Temporallogiken<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Techreport3063&diff=44972 2026-09-11T12:27:45Z

<p>Tim Lyon: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Tim |ErsterAutorNachname=Lyon |FurtherAuthors=Lukas Zenger }} {{Techreport |Title=Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents |Year=2026 |Institution=TU Dresden |Note=Full, Appended Version }} {{Publikation Details |Abstract=We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear tempor…“</p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Lukas Zenger<br /> }}<br /> {{Techreport<br /> |Title=Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents<br /> |Year=2026<br /> |Institution=TU Dresden<br /> |Note=Full, Appended Version<br /> }}<br /> {{Publikation Details<br /> |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 &quot;cycle recognition&quot; and &quot;unraveling.&quot; 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 &quot;saturation recurrence,&quot; 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.<br /> |Forschungsgruppe=Computational Logic<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Modal- und Temporallogiken<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44626 2026-07-09T14:09:12Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=&lt;p&gt;Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.&lt;/p&gt;<br /> <br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=&lt;p&gt;Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.&lt;/p&gt;<br /> <br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44625 2026-07-09T14:08:52Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=&lt;p&gt;Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.&lt;/p&gt;<br /> <br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.<br /> <br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44624 2026-07-09T14:07:47Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien. <br /> <br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna. <br /> <br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44623 2026-07-09T14:06:10Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.<br /> <br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.<br /> <br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44622 2026-07-09T14:04:14Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.<br /> &lt;br&gt;<br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> &lt;br&gt;<br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.<br /> &lt;br&gt;<br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> &lt;br&gt;<br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44621 2026-07-09T14:02:57Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.<br /> &lt;br&gt;<br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> &lt;br&gt;<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.<br /> &lt;br&gt;<br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> &lt;br&gt;<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44620 2026-07-09T14:02:36Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.&lt;br&gt;<br /> <br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> &lt;br&gt;<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.&lt;br&gt;<br /> <br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> &lt;br&gt;<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44619 2026-07-09T14:02:05Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.<br /> <br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> &lt;br&gt;<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.<br /> <br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> &lt;br&gt;<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44618 2026-07-09T14:01:49Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.&lt;br&gt;<br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> &lt;br&gt;<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.&lt;br&gt;<br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> &lt;br&gt;<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44617 2026-07-09T14:01:09Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.<br /> &lt;br&gt;<br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> &lt;br&gt;<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.<br /> &lt;br&gt;<br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> &lt;br&gt;<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News113&diff=44615 2026-07-09T13:59:15Z

<p>Tim Lyon: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien. &lt;br&gt; Standpoint…“</p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Kurs über Standpoint Logic auf der ESSAI 2026 von Tim Lyon und Hannes Straß<br /> |Titel EN=Course on Standpoint Logic at ESSAI 2026 by Tim Lyon and Hannes Straß<br /> |Beschreibung DE=Tim Lyon und Hannes Straß hielten einen Kurs mit dem Titel „Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; auf der ESSAI 2026, der European Summer School on Artificial Intelligence, in Wien.<br /> &lt;br&gt;<br /> <br /> Standpoint Logic ist ein multimodales Framework für das Schließen mit diversen und potenziell widersprüchlichen Wissensperspektiven, ohne diese in eine einzelne Sichtweise zusammenführen zu müssen. Der Kurs bot eine Einführung in die propositionale und prädikatenlogische Variante der Standpoint Logic, Beweistheorie mittels geschachtelter Sequenzen, Standpoint-Beschreibungslogiken sowie nicht-monotone Standpoint-Logik.<br /> &lt;br&gt;<br /> <br /> Vorlesungsvideos, Folien und relevante Publikationen sind auf der [https://sites.google.com/view/essai-26-standpoint-logic/home Kurs-Webseite] verfügbar. Weitere Informationen zum Kurs finden sich auf der [https://essai2026.eu/program.php#id-C9 ESSAI 2026 Programmseite].<br /> |Beschreibung EN=Tim Lyon and Hannes Straß held a course entitled &quot;Multi-Perspective Reasoning in Knowledge Representation: An Introduction to Standpoint Logic&quot; at ESSAI 2026, the European Summer School on Artificial Intelligence, in Vienna.<br /> &lt;br&gt;<br /> <br /> Standpoint Logic is a multi-modal framework for reasoning with diverse and potentially conflicting knowledge perspectives without requiring them to be merged into a single view. The course provided an introduction to the propositional and first-order variants of standpoint logic, proof theory via nested sequents, standpoint description logics, and non-monotonic standpoint logic.<br /> &lt;br&gt;<br /> <br /> Lecture videos, slides, and relevant papers are available on the [https://sites.google.com/view/essai-26-standpoint-logic/home course webpage]. Further details about the course can be found on the [https://essai2026.eu/program.php#id-C9 ESSAI 2026 programme page].<br /> |URL=https://sites.google.com/view/essai-26-standpoint-logic/home<br /> |Datum=2026-07-09<br /> |Bild=Screenshot 2026-07-09 at 15.58.01.png<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:Screenshot_2026-07-09_at_15.58.01.png&diff=44614 2026-07-09T13:59:11Z

<p>Tim Lyon: </p> <hr /> <div></div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News112&diff=44613 2026-07-09T10:05:57Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Jonas Karge verteidigt erfolgreich seine Dissertation über Multi-Agent Belief Management<br /> |Titel EN=Jonas Karge Successfully Defends PhD Thesis on Multi-Agent Belief Management<br /> |Beschreibung DE=Wir freuen uns, bekannt geben zu dürfen, dass Jonas Karge seine Dissertation mit dem Titel „Multi-Agent Belief Management&quot; erfolgreich verteidigt hat. In seiner Arbeit untersuchte Jonas, wie Gruppen zu verlässlichen Schlussfolgerungen gelangen können, wenn individuelle Urteile unsicher, qualitativ ungleich oder durch gemeinsame Verzerrungen geprägt sind. Seine Arbeit entwickelt mathematische Modelle, die erklären, wann kollektive Entscheidungen trotz unterschiedlicher Expertise, Abhängigkeiten zwischen Abstimmenden und unvollständiger Informationen die Wahrheit noch nachverfolgen können.<br /> &lt;br&gt;<br /> <br /> Die Dissertation führt darüber hinaus neue Methoden zur Kombination impräziser Wahrscheinlichkeitsschätzungen ein und untersucht, wie Faktoren wie Diversität, geteilter Einfluss und Aggregationsdesign die Genauigkeit und Robustheit von Gruppenentscheidungen beeinflussen. Die Arbeit wurde durch SECAI (School of Embedded Composite AI) und den DAAD (Deutscher Akademischer Austauschdienst) gefördert. Wir gratulieren Dr. Karge herzlich und wünschen ihm für alle zukünftigen Vorhaben viel Erfolg.<br /> <br /> Siehe auch unsere Beiträge hierzu in den sozialen Medien:<br /> * [https://bsky.app/profile/clgroup-tud.bsky.social/post/3mq2nqeo5yk2l Bluesky]<br /> * [https://www.linkedin.com/feed/update/urn:li:activity:7479343403340627968 LinkedIn]<br /> |Beschreibung EN=We are pleased to announce that Jonas Karge has successfully defended his doctoral thesis entitled &quot;Multi-Agent Belief Management.&quot; In his dissertation, Jonas investigated how groups can reach reliable conclusions when individual judgments are uncertain, uneven in quality, or shaped by shared bias. His work develops mathematical models that explain when collective decisions can still track the truth despite differences in expertise, dependence between voters, and incomplete information.<br /> &lt;br&gt;<br /> <br /> The thesis also introduces new methods for combining imprecise probability estimates and studies how factors such as diversity, shared influence, and aggregation design affect the accuracy and robustness of group decisions. The work was funded by SECAI (School of Embedded Composite AI) and DAAD (German Academic Exchange Service). We extend our warmest congratulations to Dr. Karge and wish him every success in his future endeavors.<br /> <br /> See also our posts about this on social media:<br /> * [https://bsky.app/profile/clgroup-tud.bsky.social/post/3mq2nqeo5yk2l Bluesky]<br /> * [https://www.linkedin.com/feed/update/urn:li:activity:7479343403340627968 LinkedIn]<br /> |Datum=2026-07-07<br /> |Bild=1783214424880.jpg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Tim_Lyon&diff=44607 2026-07-08T12:49:04Z

<p>Tim Lyon: </p> <hr /> <div>{{Mitarbeiter<br /> |Vorname=Tim<br /> |Nachname=Lyon<br /> |Akademischer Titel=Dr.<br /> |Forschungsgruppe=Computational Logic<br /> |Stellung=Wissenschaftlicher Mitarbeiter<br /> |Ehemaliger=0<br /> |Email=timothy_stephen.lyon@tu-dresden.de<br /> |Raum=APB 2031<br /> |Bild=Profession Pic 400x600.png<br /> |Info=I am a postdoctoral researcher in the Computational Logic group at Technische Universität Dresden. I previously worked within the ERC project DeciGUT. My research interests concern the construction and application of (non-)wellfounded proof systems for fragments of first-order logic, non-classical logics, modal logics, and fixed-point logics. Prior to joining TU Dresden, I was a PhD student at Technische Universität Wien, where I worked on the TICAMORE (Translating and Discovering Calculi for Modal and Related Logics) project under the supervision of Prof. Agata Ciabattoni.<br /> |Info EN=I am a postdoctoral researcher in the Computational Logic group at Technische Universität Dresden. I previously worked within the ERC project DeciGUT. My research interests concern the construction and application of (non-)wellfounded proof systems for fragments of first-order logic, non-classical logics, modal logics, and fixed-point logics. Prior to joining TU Dresden, I was a PhD student at Technische Universität Wien, where I worked on the TICAMORE (Translating and Discovering Calculi for Modal and Related Logics) project under the supervision of Prof. Agata Ciabattoni.<br /> |DBLP=https://dblp.org/pid/211/4650.html<br /> |Google Scholar=https://scholar.google.com/citations?hl=en&amp;user=kutoU-wAAAAJ<br /> |Alternative URI=https://sites.google.com/view/timlyon<br /> |Publikationen anzeigen=1<br /> |Abschlussarbeiten anzeigen=1<br /> |Projekte anzeigen=0<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Existenzielle Regeln<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beschreibungslogiken<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Modal- und Temporallogiken<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Datenbanktheorie<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Wissensrepräsentation und logisches Schließen<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Multiagentensysteme<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Article3099&diff=44606 2026-07-08T12:44:20Z

<p>Tim Lyon: </p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Kees van Berkel<br /> }}<br /> {{Article<br /> |Referiert=1<br /> |Title=Proof Theory and Decision Procedures for Deontic STIT Logics<br /> |To appear=0<br /> |Year=2024<br /> |Journal=Journal of Artificial Intelligence Research<br /> |Volume=81<br /> }}<br /> {{Publikation Details<br /> |Abstract=This paper provides a set of cut-free complete sequent-style calculi for deontic STIT (`See To It That') logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write a proof-search algorithm deciding deontic, multi-agent STIT logics with (un)limited choice and introduce a special loop-checking mechanism to ensure the termination of the algorithm. Despite the acknowledged potential for deontic reasoning in the context of autonomous, multi-agent scenarios, this work is the first to provide a syntactic decision procedure for this class of logics. Our proof-search procedure is designed to provide verifiable witnesses/certificates of the (in)validity of formulae, which permits an analysis of the (non)theoremhood of formulae and act as explanations thereof. We show how the proof system and decision algorithm can be used to automate normative reasoning tasks such as duty checking (viz. determining an agent's obligations relative to a given knowledge base), compliance checking (viz. determining if a choice, considered by an agent as potential conduct, complies with the given knowledge base), and joint fulfillment checking (viz. determining whether under a specified factual context an agent can jointly fulfill all their duties).<br /> |Download=JAIR24-LyoBer.pdf<br /> |Link=https://arxiv.org/abs/2402.03148<br /> |DOI Name=https://doi.org/10.1613/jair.1.15710<br /> |Projekt=DeciGUT<br /> |Forschungsgruppe=Computational Logic<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Modal- und Temporallogiken<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Multiagentensysteme<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Article3123&diff=44605 2026-07-08T12:43:39Z

<p>Tim Lyon: </p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Piotr Ostropolski-Nalewaja<br /> }}<br /> {{Article<br /> |Referiert=1<br /> |Title=Foundations for an Abstract Proof Theory in the Context of Horn Rules<br /> |To appear=1<br /> |Year=2026<br /> |Month=Juni<br /> |Journal=ACM Transactions on Computational Logic<br /> }}<br /> {{Publikation Details<br /> |Abstract=We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed &quot;g-sequents,&quot; which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of inference rule types as sets of operations that act over such objects, and define abstract (sequent) calculi as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any multisequent proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.<br /> |Projekt=DeciGUT<br /> |Forschungsgruppe=Computational Logic<br /> }}<br /> {{Forschungsgebiet Auswahl<br /> |Forschungsgebiet=Beweistheorie<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44604 2026-07-07T13:50:28Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, CMS-LM-ADV, CMS-LM-MOC, INF-BAS6, INF-PM-FOR, INF-VERT6<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-05-15<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-05<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-12<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-19<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-26<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-07-03<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-07-17<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News112&diff=44603 2026-07-07T13:04:20Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Jonas Karge verteidigt erfolgreich seine Dissertation über Multi-Agent Belief Management<br /> |Titel EN=Jonas Karge Successfully Defends PhD Thesis on Multi-Agent Belief Management<br /> |Beschreibung DE=Wir freuen uns, bekannt geben zu dürfen, dass Jonas Karge seine Dissertation mit dem Titel „Multi-Agent Belief Management&quot; erfolgreich verteidigt hat. In seiner Arbeit untersuchte Jonas, wie Gruppen zu verlässlichen Schlussfolgerungen gelangen können, wenn individuelle Urteile unsicher, qualitativ ungleich oder durch gemeinsame Verzerrungen geprägt sind. Seine Arbeit entwickelt mathematische Modelle, die erklären, wann kollektive Entscheidungen trotz unterschiedlicher Expertise, Abhängigkeiten zwischen Abstimmenden und unvollständiger Informationen die Wahrheit noch nachverfolgen können.<br /> &lt;br&gt;<br /> <br /> Die Dissertation führt darüber hinaus neue Methoden zur Kombination impräziser Wahrscheinlichkeitsschätzungen ein und untersucht, wie Faktoren wie Diversität, geteilter Einfluss und Aggregationsdesign die Genauigkeit und Robustheit von Gruppenentscheidungen beeinflussen. Die Arbeit wurde durch SECAI (School of Embedded Composite AI) und den DAAD (Deutscher Akademischer Austauschdienst) gefördert. Wir gratulieren Dr. Karge herzlich und wünschen ihm für alle zukünftigen Vorhaben viel Erfolg.<br /> |Beschreibung EN=We are pleased to announce that Jonas Karge has successfully defended his doctoral thesis entitled &quot;Multi-Agent Belief Management.&quot; In his dissertation, Jonas investigated how groups can reach reliable conclusions when individual judgments are uncertain, uneven in quality, or shaped by shared bias. His work develops mathematical models that explain when collective decisions can still track the truth despite differences in expertise, dependence between voters, and incomplete information.<br /> &lt;br&gt;<br /> <br /> The thesis also introduces new methods for combining imprecise probability estimates and studies how factors such as diversity, shared influence, and aggregation design affect the accuracy and robustness of group decisions. The work was funded by SECAI (School of Embedded Composite AI) and DAAD (German Academic Exchange Service). We extend our warmest congratulations to Dr. Karge and wish him every success in his future endeavors.<br /> |Datum=2026-07-07<br /> |Bild=1783214424880.jpg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News112&diff=44601 2026-07-07T13:03:30Z

<p>Tim Lyon: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Jonas Karge verteidigt erfolgreich seine Dissertation über Multi-Agent Belief Management |Titel EN=Jonas Karge Successfully Defends PhD Thesis on Multi-Agent Belief Management |Beschreibung DE=Wir freuen uns, bekannt geben zu dürfen, dass Jonas Karge seine Dissertation mit dem Titel „Multi-Agent Belief Management&quot; erfolgreich verteidigt hat. In seiner Arbeit untersuchte Jonas, wie Gruppen zu verlässlichen Schlussfolgerungen gela…“</p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Jonas Karge verteidigt erfolgreich seine Dissertation über Multi-Agent Belief Management<br /> |Titel EN=Jonas Karge Successfully Defends PhD Thesis on Multi-Agent Belief Management<br /> |Beschreibung DE=Wir freuen uns, bekannt geben zu dürfen, dass Jonas Karge seine Dissertation mit dem Titel „Multi-Agent Belief Management&quot; erfolgreich verteidigt hat. In seiner Arbeit untersuchte Jonas, wie Gruppen zu verlässlichen Schlussfolgerungen gelangen können, wenn individuelle Urteile unsicher, qualitativ ungleich oder durch gemeinsame Verzerrungen geprägt sind. Seine Arbeit entwickelt mathematische Modelle, die erklären, wann kollektive Entscheidungen trotz unterschiedlicher Expertise, Abhängigkeiten zwischen Abstimmenden und unvollständiger Informationen die Wahrheit noch nachverfolgen können.<br /> &lt;\br&gt;<br /> <br /> Die Dissertation führt darüber hinaus neue Methoden zur Kombination impräziser Wahrscheinlichkeitsschätzungen ein und untersucht, wie Faktoren wie Diversität, geteilter Einfluss und Aggregationsdesign die Genauigkeit und Robustheit von Gruppenentscheidungen beeinflussen. Die Arbeit wurde durch SECAI (School of Embedded Composite AI) und den DAAD (Deutscher Akademischer Austauschdienst) gefördert. Wir gratulieren Dr. Karge herzlich und wünschen ihm für alle zukünftigen Vorhaben viel Erfolg.<br /> |Beschreibung EN=We are pleased to announce that Jonas Karge has successfully defended his doctoral thesis entitled &quot;Multi-Agent Belief Management.&quot; In his dissertation, Jonas investigated how groups can reach reliable conclusions when individual judgments are uncertain, uneven in quality, or shaped by shared bias. His work develops mathematical models that explain when collective decisions can still track the truth despite differences in expertise, dependence between voters, and incomplete information.<br /> &lt;\br&gt;<br /> <br /> The thesis also introduces new methods for combining imprecise probability estimates and studies how factors such as diversity, shared influence, and aggregation design affect the accuracy and robustness of group decisions. The work was funded by SECAI (School of Embedded Composite AI) and DAAD (German Academic Exchange Service). We extend our warmest congratulations to Dr. Karge and wish him every success in his future endeavors.<br /> |Datum=2026-07-07<br /> |Bild=1783214424880.jpg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:1783214424880.jpg&diff=44600 2026-07-07T13:02:39Z

<p>Tim Lyon: </p> <hr /> <div></div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News111&diff=44577 2026-07-02T11:17:46Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß erhält Lehrpreis des Fachschaftsrats für „Algorithmische Spieltheorie&quot;<br /> |Titel EN=Hannes Straß Receives Student Council Teaching Award for &quot;Algorithmic Game Theory&quot;<br /> |Beschreibung DE=Hannes Straß, Wissenschaftler in der Arbeitsgruppe Computational Logic am ICCL, hat den Lehrpreis des Fachschaftsrats in der Kategorie „Beste Wahlpflichtveranstaltung&quot; für seine Vorlesung „Algorithmische Spieltheorie&quot; erhalten.<br /> &lt;br&gt;<br /> Der Preis wurde im Rahmen der OUTPUT.DD-Veranstaltung der Fakultät verliehen. Die Lehrpreise des Fachschaftsrats würdigen herausragende Lehre auf Grundlage studentischer Bewertungen, wobei verschiedene Kategorien Exzellenz in unterschiedlichen Veranstaltungsformaten auszeichnen.<br /> <br /> Herzlichen Glückwunsch, Hannes!<br /> |Beschreibung EN=Hannes Straß, who is a researcher in the Computational Logic Group at the ICCL, has received the Student Council's teaching award in the category &quot;Best Elective&quot; for his lecture &quot;Algorithmic Game Theory.&quot;<br /> &lt;br&gt;<br /> The award was presented at the department's OUTPUT.DD event. The Student Council's teaching awards recognize outstanding teaching as evaluated by students, with categories honoring excellence across different course formats.<br /> <br /> Congratulations Hannes!<br /> |Datum=2026-07-02<br /> |Bild=Pic hannes.jpeg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News111&diff=44576 2026-07-02T11:17:22Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß erhält Lehrpreis des Fachschaftsrats für „Algorithmische Spieltheorie&quot;<br /> |Titel EN=Hannes Straß Receives Student Council Teaching Award for &quot;Algorithmic Game Theory&quot;<br /> |Beschreibung DE=Hannes Straß, Wissenschaftler in der Arbeitsgruppe Computational Logic am ICCL, hat den Lehrpreis des Fachschaftsrats in der Kategorie „Beste Wahlpflichtveranstaltung&quot; für seine Vorlesung „Algorithmische Spieltheorie&quot; erhalten.<br /> &lt;br&gt;<br /> <br /> Der Preis wurde im Rahmen der OUTPUT.DD-Veranstaltung der Fakultät verliehen. Die Lehrpreise des Fachschaftsrats würdigen herausragende Lehre auf Grundlage studentischer Bewertungen, wobei verschiedene Kategorien Exzellenz in unterschiedlichen Veranstaltungsformaten auszeichnen.<br /> <br /> Herzlichen Glückwunsch, Hannes!<br /> |Beschreibung EN=Hannes Straß, who is a researcher in the Computational Logic Group at the ICCL, has received the Student Council's teaching award in the category &quot;Best Elective&quot; for his lecture &quot;Algorithmic Game Theory.&quot;<br /> &lt;br&gt;<br /> <br /> The award was presented at the department's OUTPUT.DD event. The Student Council's teaching awards recognize outstanding teaching as evaluated by students, with categories honoring excellence across different course formats.<br /> <br /> Congratulations Hannes!<br /> |Datum=2026-07-02<br /> |Bild=Pic hannes.jpeg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News111&diff=44575 2026-07-02T11:16:46Z

<p>Tim Lyon: </p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß erhält Lehrpreis des Fachschaftsrats für „Algorithmische Spieltheorie&quot;<br /> |Titel EN=Hannes Straß Receives Student Council Teaching Award for &quot;Algorithmic Game Theory&quot;<br /> |Beschreibung DE=Hannes Straß, Wissenschaftler in der Arbeitsgruppe Computational Logic am ICCL, hat den Lehrpreis des Fachschaftsrats in der Kategorie „Beste Wahlpflichtveranstaltung&quot; für seine Vorlesung „Algorithmische Spieltheorie&quot; erhalten. &lt;br&gt;<br /> <br /> Der Preis wurde im Rahmen der OUTPUT.DD-Veranstaltung der Fakultät verliehen. Die Lehrpreise des Fachschaftsrats würdigen herausragende Lehre auf Grundlage studentischer Bewertungen, wobei verschiedene Kategorien Exzellenz in unterschiedlichen Veranstaltungsformaten auszeichnen.<br /> <br /> Herzlichen Glückwunsch, Hannes!<br /> |Beschreibung EN=Hannes Straß, who is a researcher in the Computational Logic Group at the ICCL, has received the Student Council's teaching award in the category &quot;Best Elective&quot; for his lecture &quot;Algorithmic Game Theory.&quot; &lt;br&gt;<br /> <br /> The award was presented at the department's OUTPUT.DD event. The Student Council's teaching awards recognize outstanding teaching as evaluated by students, with categories honoring excellence across different course formats.<br /> <br /> Congratulations Hannes!<br /> |Datum=2026-07-02<br /> |Bild=Pic hannes.jpeg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=News111&diff=44573 2026-07-02T11:15:46Z

<p>Tim Lyon: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Hannes Straß erhält Lehrpreis des Fachschaftsrats für „Algorithmische Spieltheorie&quot; |Titel EN=Hannes Straß Receives Student Council Teaching Award for &quot;Algorithmic Game Theory&quot; |Beschreibung DE=Hannes Straß, Wissenschaftler in der Arbeitsgruppe Computational Logic am ICCL, hat den Lehrpreis des Fachschaftsrats in der Kategorie „Beste Wahlpflichtveranstaltung&quot; für seine Vorlesung „Algorithmische Spieltheorie&quot; erhalten.…“</p> <hr /> <div>{{Neuigkeit<br /> |Titel DE=Hannes Straß erhält Lehrpreis des Fachschaftsrats für „Algorithmische Spieltheorie&quot;<br /> |Titel EN=Hannes Straß Receives Student Council Teaching Award for &quot;Algorithmic Game Theory&quot;<br /> |Beschreibung DE=Hannes Straß, Wissenschaftler in der Arbeitsgruppe Computational Logic am ICCL, hat den Lehrpreis des Fachschaftsrats in der Kategorie „Beste Wahlpflichtveranstaltung&quot; für seine Vorlesung „Algorithmische Spieltheorie&quot; erhalten.<br /> <br /> Der Preis wurde im Rahmen der OUTPUT.DD-Veranstaltung der Fakultät verliehen. Die Lehrpreise des Fachschaftsrats würdigen herausragende Lehre auf Grundlage studentischer Bewertungen, wobei verschiedene Kategorien Exzellenz in unterschiedlichen Veranstaltungsformaten auszeichnen.<br /> <br /> Herzlichen Glückwunsch, Hannes!<br /> |Beschreibung EN=Hannes Straß, who is a researcher in the Computational Logic Group at the ICCL, has received the Student Council's teaching award in the category &quot;Best Elective&quot; for his lecture &quot;Algorithmic Game Theory.&quot;<br /> <br /> The award was presented at the department's OUTPUT.DD event. The Student Council's teaching awards recognize outstanding teaching as evaluated by students, with categories honoring excellence across different course formats.<br /> <br /> Congratulations Hannes!<br /> |Datum=2026-07-02<br /> |Bild=Pic hannes.jpeg<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Datei:Pic_hannes.jpeg&diff=44572 2026-07-02T11:10:00Z

<p>Tim Lyon: </p> <hr /> <div></div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44513 2026-06-19T07:32:11Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-05<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-12<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-19<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-26<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-07-03<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-07-17<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44512 2026-06-19T07:31:28Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-05<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-12<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-19<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-06-26<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture<br /> |Room=APB E001<br /> |Date=2026-07-03<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44511 2026-06-18T20:27:18Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 3<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 4<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 5<br /> |Room=APB E001<br /> |Date=2026-06-05<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 6<br /> |Room=APB E001<br /> |Date=2026-06-12<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 7<br /> |Room=APB E001<br /> |Date=2026-06-19<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 8<br /> |Room=APB E001<br /> |Date=2026-06-26<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 9<br /> |Room=APB E001<br /> |Date=2026-07-03<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44467 2026-06-05T12:39:45Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 3<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 4<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 5<br /> |Room=APB E001<br /> |Date=2026-06-05<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 6<br /> |Room=APB E001<br /> |Date=2026-06-12<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Article3123&diff=44460 2026-06-04T10:09:36Z

<p>Tim Lyon: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Tim |ErsterAutorNachname=Lyon |FurtherAuthors=Piotr Ostropolski-Nalewaja }} {{Article |Referiert=1 |Title=Foundations for an Abstract Proof Theory in the Context of Horn Rules |To appear=1 |Year=2026 |Month=Juni |Journal=ACM Transactions on Computational Logic }} {{Publikation Details |Abstract=We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a numbe…“</p> <hr /> <div>{{Publikation Erster Autor<br /> |ErsterAutorVorname=Tim<br /> |ErsterAutorNachname=Lyon<br /> |FurtherAuthors=Piotr Ostropolski-Nalewaja<br /> }}<br /> {{Article<br /> |Referiert=1<br /> |Title=Foundations for an Abstract Proof Theory in the Context of Horn Rules<br /> |To appear=1<br /> |Year=2026<br /> |Month=Juni<br /> |Journal=ACM Transactions on Computational Logic<br /> }}<br /> {{Publikation Details<br /> |Abstract=We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed &quot;g-sequents,&quot; which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of inference rule types as sets of operations that act over such objects, and define abstract (sequent) calculi as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any multisequent proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.<br /> |Projekt=DeciGUT<br /> |Forschungsgruppe=Computational Logic<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44431 2026-05-21T09:10:00Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 3<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 4<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 5<br /> |Room=APB E001<br /> |Date=2026-06-05<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44430 2026-05-21T08:34:46Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 3<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 4<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 5<br /> |Room=APB E001<br /> |Date=2026-05-05<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44424 2026-05-20T20:01:30Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 3<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 4<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 5<br /> |Room=APB E001<br /> |Date=2026-05-29<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44369 2026-04-30T08:45:01Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 3<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 4<br /> |Room=APB E001<br /> |Date=2026-05-22<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44368 2026-04-30T08:44:19Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 3<br /> |Room=APB E001<br /> |Date=2026-05-08<br /> |DS=DS3<br /> }}</div>

Tim Lyon https://iccl.inf.tu-dresden.de/w/index.php?title=Proof_Theory_and_Sequent_Systems_(SS2026)&diff=44320 2026-04-20T18:18:54Z

<p>Tim Lyon: </p> <hr /> <div>{{Vorlesung<br /> |Title=Proof Theory and Sequent Systems<br /> |Research group=Computational Logic<br /> |Lecturers=Tim Lyon<br /> |Term=SS<br /> |Year=2026<br /> |Module=INF-25-Ma-FTK-ASAI, INF-BAS2, INF-VERT2<br /> |SWSLecture=2<br /> |SWSExercise=0<br /> |SWSPractical=0<br /> |Exam type=mündliche Prüfung<br /> |Description====Course Description===<br /> <br /> Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.<br /> <br /> In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?<br /> <br /> ===Prerequisites===<br /> <br /> Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.<br /> <br /> ===Course Plan===<br /> <br /> The course will take place on Fridays 11:10 – 12:40 in room APB E001. The first class will take place on 17 April 2026.<br /> <br /> ===Examination===<br /> <br /> There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.<br /> |Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 1<br /> |Room=APB E001<br /> |Date=2026-04-17<br /> |DS=DS3<br /> }}<br /> {{Vorlesung Zeiten<br /> |Lehrveranstaltungstype=Vorlesung<br /> |Title=Lecture 2<br /> |Room=APB E001<br /> |Date=2026-04-24<br /> |DS=DS3<br /> }}</div>

Tim Lyon