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

Proof Theory and Sequent Systems (SS2026)

2026-03-28T09:56:18Z

Tim Lyon: Die Seite wurde neu angelegt: „{{Vorlesung |Title=Proof Theory and Sequent Systems |Research group=Computational Logic |Lecturers=Tim Lyon |Term=SS |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…“

{{Vorlesung
|Title=Proof Theory and Sequent Systems
|Research group=Computational Logic
|Lecturers=Tim Lyon
|Term=SS
|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 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.

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?

===Prerequisites===

Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.

===Course Plan===

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.

===Examination===

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.
|Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 1
|Room=APB E001
|Date=2026-04-17
|DS=DS3
}}

Proof Theory and Sequent Systems (WS2025)

2026-03-28T09:45:29Z

Tim Lyon:

{{Vorlesung
|Title=Proof Theory and Sequent Systems
|Research group=Computational Logic
|Lecturers=Tim Lyon
|Term=WS
|Year=2025
|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 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.

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?

===Prerequisites===

Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.

===Course Plan===

The course will take place on Fridays 9:20 – 10:50 in room APB E007. The first class will take place on 24 October 2025.

===Examination===

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.
|Literature=*The course script can be downloaded from the following website: [https://sites.google.com/view/timlyon/teaching?authuser=0 [Link to Script]]
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 1
|Room=APB E007
|Date=2025-10-24
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 2
|Room=APB E007
|Date=2025-11-07
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 3
|Room=APB E007
|Date=2025-11-14
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 4
|Room=APB E007
|Date=2025-11-21
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 5
|Room=APB E007
|Date=2025-11-28
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 6
|Room=APB E007
|Date=2025-12-05
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 7
|Room=APB E007
|Date=2025-12-12
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 8
|Room=APB E007
|Date=2025-12-19
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 9
|Room=APB E007
|Date=2026-01-09
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 10
|Room=APB E007
|Date=2026-01-16
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture 11
|Room=APB E007
|Date=2026-01-23
|DS=DS2
}}

Thema3519

2026-02-26T11:29:48Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving
|Titel EN=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving
|Abschlussarbeitstyp=Master
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Offen
|Ergebnisse=Thesis Topics Lyon.pdf
|Beschreibung DE=<h2>Overview</h2>
<p>
I supervise Master’s thesis projects in areas related to <strong>symbolic logic, proof theory, and automated reasoning</strong>. Students interested in formal methods, non-classical logics, decision procedures, verification, or theorem proving are encouraged to contact me to discuss potential projects.
</p>
<p>Research topics can range from foundational studies in logic to practical implementation of reasoning tools. Examples include, but are not limited to:</p>

<ul>
<li>Study and implementation of proof calculi for non-classical logics.</li>
<li>Theoretical investigations of non-classical logics used in computer science and knowledge representation.</li>
<li>Investigation of decision algorithms, proof search strategies, and complexity results.</li>
<li>Development of theorem provers for modal or related logics.</li>
<li>Study and verification (e.g., in Ada/SPARK) of proof transformation algorithms.</li>
</ul>

<h2>Getting in Touch</h2>
<p>
If you are interested in undertaking a thesis project in any of the areas listed above, or wish to propose a related project of your own, please contact me via email to discuss possible topics:
</p>

<ul>
<li><strong>Email:</strong> timothy_stephen.lyon@tu-dresden.de</li>
<li><strong>Office:</strong> APB 2031, Andreas-Pfitzmann-Bau, Fakultät für Informatik, TU Dresden</li>
</ul>

<p>In your email, please briefly introduce yourself, indicate your degree program, and mention any prior experience in logic, programming, or formal methods.</p>

<h2>Further Information</h2>
<p>
Note that the above information is included in a PDF, which can be downloaded with the "download" link on this webpage. For further information, including research interests, descriptions of past projects, and related resources, please see my research page: https://sites.google.com/view/timlyon/home?authuser=0
</p>
|Beschreibung EN=<h2>Overview</h2>
<p>
I supervise Master’s thesis projects in areas related to <strong>symbolic logic, proof theory, and automated reasoning</strong>. Students interested in formal methods, non-classical logics, decision procedures, verification, or theorem proving are encouraged to contact me to discuss potential projects.
</p>
<p>Research topics can range from foundational studies in logic to practical implementation of reasoning tools. Examples include, but are not limited to:</p>

<ul>
<li>Study and implementation of proof calculi for non-classical logics.</li>
<li>Theoretical investigations of non-classical logics used in computer science and knowledge representation.</li>
<li>Investigation of decision algorithms, proof search strategies, and complexity results.</li>
<li>Development of theorem provers for modal or related logics.</li>
<li>Study and verification (e.g., in Ada/SPARK) of proof transformation algorithms.</li>
</ul>

<h2>Getting in Touch</h2>
<p>
If you are interested in undertaking a thesis project in any of the areas listed above, or wish to propose a related project of your own, please contact me via email to discuss possible topics:
</p>

<ul>
<li><strong>Email:</strong> timothy_stephen.lyon@tu-dresden.de</li>
<li><strong>Office:</strong> APB 2031, Andreas-Pfitzmann-Bau, Fakultät für Informatik, TU Dresden</li>
</ul>

<p>In your email, please briefly introduce yourself, indicate your degree program, and mention any prior experience in logic, programming, or formal methods.</p>

<h2>Further Information</h2>
<p>
Note that the above information is included in a PDF, which can be downloaded with the "download" link on this webpage. For further information, including research interests, descriptions of past projects, and related resources, please see my research page: https://sites.google.com/view/timlyon/home?authuser=0
</p>
}}

Thema3519

2026-02-26T11:29:10Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving
|Titel EN=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving
|Abschlussarbeitstyp=Master
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Offen
|Ergebnisse=Thesis Topics Lyon.pdf
|Beschreibung DE=<h2>Overview</h2>
<p>
I supervise Master’s thesis projects in areas related to <strong>symbolic logic, proof theory, and automated reasoning</strong>. Students interested in formal methods, non-classical logics, decision procedures, verification, or theorem proving are encouraged to contact me to discuss potential projects.
</p>
<p>Research topics can range from foundational studies in logic to practical implementation of reasoning tools. Examples include, but are not limited to:</p>

<ul>
<li>Study and implementation of proof calculi for non-classical logics.</li>
<li>Theoretical investigations of non-classical logics used in computer science and knowledge representation.</li>
<li>Investigation of decision algorithms, proof search strategies, and complexity results.</li>
<li>Development of theorem provers for modal or related logics.</li>
<li>Study and verification (e.g., in Ada/SPARK) of proof transformation algorithms.</li>
</ul>

<h2>Getting in Touch</h2>
<p>
If you are interested in undertaking a thesis project in any of the areas listed above, or wish to propose a related project of your own, please contact me via email to discuss possible topics:
</p>

<ul>
<li><strong>Email:</strong> <a href="mailto:timothy_stephen.lyon@tu-dresden.de">timothy_stephen.lyon@tu-dresden.de</a></li>
<li><strong>Office:</strong> APB 2031, Andreas-Pfitzmann-Bau, Fakultät für Informatik, TU Dresden</li>
</ul>

<p>In your email, please briefly introduce yourself, indicate your degree program, and mention any prior experience in logic, programming, or formal methods.</p>

<h2>Further Information</h2>
<p>
Note that the above information is included in a PDF, which can be downloaded with the "download" link on this webpage. For further information, including research interests, descriptions of past projects, and related resources, please see my research page: <a href="https://sites.google.com/view/timlyon/home?authuser=0">https://sites.google.com/view/timlyon/home?authuser=0</a>
</p>
|Beschreibung EN=<h2>Overview</h2>
<p>
I supervise Master’s thesis projects in areas related to <strong>symbolic logic, proof theory, and automated reasoning</strong>. Students interested in formal methods, non-classical logics, decision procedures, verification, or theorem proving are encouraged to contact me to discuss potential projects.
</p>
<p>Research topics can range from foundational studies in logic to practical implementation of reasoning tools. Examples include, but are not limited to:</p>

<ul>
<li>Study and implementation of proof calculi for non-classical logics.</li>
<li>Theoretical investigations of non-classical logics used in computer science and knowledge representation.</li>
<li>Investigation of decision algorithms, proof search strategies, and complexity results.</li>
<li>Development of theorem provers for modal or related logics.</li>
<li>Study and verification (e.g., in Ada/SPARK) of proof transformation algorithms.</li>
</ul>

<h2>Getting in Touch</h2>
<p>
If you are interested in undertaking a thesis project in any of the areas listed above, or wish to propose a related project of your own, please contact me via email to discuss possible topics:
</p>

<ul>
<li><strong>Email:</strong> timothy_stephen.lyon@tu-dresden.de</li>
<li><strong>Office:</strong> APB 2031, Andreas-Pfitzmann-Bau, Fakultät für Informatik, TU Dresden</li>
</ul>

<p>In your email, please briefly introduce yourself, indicate your degree program, and mention any prior experience in logic, programming, or formal methods.</p>

<h2>Further Information</h2>
<p>
Note that the above information is included in a PDF, which can be downloaded with the "download" link on this webpage. For further information, including research interests, descriptions of past projects, and related resources, please see my research page: <a href="https://sites.google.com/view/timlyon/home?authuser=0">https://sites.google.com/view/timlyon/home?authuser=0</a>
</p>
}}

Thema3519

2026-02-26T11:26:24Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving
|Titel EN=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving
|Abschlussarbeitstyp=Master
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Offen
|Ergebnisse=Thesis Topics Lyon.pdf
|Beschreibung DE=<h2>Overview</h2>
<p>
I supervise Master’s thesis projects in areas related to <strong>symbolic logic, proof theory, and automated reasoning</strong>. Students interested in formal methods, non-classical logics, decision procedures, verification, or theorem proving are encouraged to contact me to discuss potential projects.
</p>
<p>Research topics can range from foundational studies in logic to practical implementation of reasoning tools. Examples include, but are not limited to:</p>

<ul>
<li>Study and implementation of proof calculi for non-classical logics.</li>
<li>Theoretical investigations of non-classical logics used in computer science and knowledge representation.</li>
<li>Investigation of decision algorithms, proof search strategies, and complexity results.</li>
<li>Development of theorem provers for modal or related logics.</li>
<li>Study and verification (e.g., in Ada/SPARK) of proof transformation algorithms.</li>
</ul>

<h2>Getting in Touch</h2>
<p>
If you are interested in undertaking a thesis project in any of the areas listed above, or wish to propose a related project of your own, please contact me via email to discuss possible topics:
</p>

<ul>
<li><strong>Email:</strong> <a href="mailto:timothy_stephen.lyon@tu-dresden.de">timothy_stephen.lyon@tu-dresden.de</a></li>
<li><strong>Office:</strong> APB 2031, Andreas-Pfitzmann-Bau, Fakultät für Informatik, TU Dresden</li>
</ul>

<p>In your email, please briefly introduce yourself, indicate your degree program, and mention any prior experience in logic, programming, or formal methods.</p>

<h2>Further Information</h2>
<p>
Note that the above information is included in a PDF, which can be downloaded with the "download" link on this webpage. For further information, including research interests, descriptions of past projects, and related resources, please see my research page: <a href="https://sites.google.com/view/timlyon/home?authuser=0">https://sites.google.com/view/timlyon/home?authuser=0</a>
</p>
|Beschreibung EN=<h2>Overview</h2>
<p>
I supervise Master’s thesis projects in areas related to <strong>symbolic logic, proof theory, and automated reasoning</strong>. Students interested in formal methods, non-classical logics, decision procedures, verification, or theorem proving are encouraged to contact me to discuss potential projects.
</p>
<p>Research topics can range from foundational studies in logic to practical implementation of reasoning tools. Examples include, but are not limited to:</p>

<ul>
<li>Study and implementation of proof calculi for non-classical logics.</li>
<li>Theoretical investigations of non-classical logics used in computer science and knowledge representation.</li>
<li>Investigation of decision algorithms, proof search strategies, and complexity results.</li>
<li>Development of theorem provers for modal or related logics.</li>
<li>Study and verification (e.g., in Ada/SPARK) of proof transformation algorithms.</li>
</ul>

<h2>Getting in Touch</h2>
<p>
If you are interested in undertaking a thesis project in any of the areas listed above, or wish to propose a related project of your own, please contact me via email to discuss possible topics:
</p>

<ul>
<li><strong>Email:</strong> <a href="mailto:timothy_stephen.lyon@tu-dresden.de">timothy_stephen.lyon@tu-dresden.de</a></li>
<li><strong>Office:</strong> APB 2031, Andreas-Pfitzmann-Bau, Fakultät für Informatik, TU Dresden</li>
</ul>

<p>In your email, please briefly introduce yourself, indicate your degree program, and mention any prior experience in logic, programming, or formal methods.</p>

<h2>Further Information</h2>
<p>
Note that the above information is included in a PDF, which can be downloaded with the "download" link on this webpage. For further information, including research interests, descriptions of past projects, and related resources, please see my research page: <a href="https://sites.google.com/view/timlyon/home?authuser=0">https://sites.google.com/view/timlyon/home?authuser=0</a>
</p>
}}

Thema3519

2026-02-26T11:25:25Z

Tim Lyon:

Thema3519

2026-02-26T11:24:12Z

Tim Lyon:

Thema3519

2026-02-26T11:22:49Z

Tim Lyon:

Thema3519

2026-02-26T11:22:05Z

Tim Lyon:

Thema3519

2026-02-26T11:20:59Z

Tim Lyon:

Thema3519

2026-02-26T11:19:31Z

Tim Lyon:

Thema3519

2026-02-26T11:18:18Z

Tim Lyon:

Thema3519

2026-02-26T11:17:24Z

Tim Lyon:

Thema3519

2026-02-26T11:14:16Z

Tim Lyon:

Thema3519

2026-02-26T10:59:24Z

Tim Lyon: Die Seite wurde neu angelegt: „{{Abschlussarbeit |Titel DE=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving |Titel EN=Master's Thesis Projects in Symbolic Logic, Proof Theory, and Theorem Proving |Abschlussarbeitstyp=Master |Betreuer=Tim Lyon |Forschungsgruppe=Computational Logic |Abschlussarbeitsstatus=Offen |Beschreibung DE=Bitte sehen Sie sich die beigefügte PDF-Datei an, die Sie über den „Download“-Link herunterladen können. |Beschreibung EN=Plea…“

Datei:Thesis Topics Lyon.pdf

2026-02-26T10:58:21Z

Tim Lyon:

News109

2026-01-13T11:53:57Z

Tim Lyon:

{{Neuigkeit
|Titel DE=Tim Lyon ist dem Herausgebergremium des Bulletin of the Section of Logic beigetreten
|Titel EN=Tim Lyon has joined the editorial board of the Bulletin of the Section of Logic
|Beschreibung DE=Tim Lyon, Postdoktorand am ICCL, ist in das Herausgebergremium des Bulletin of the Section of Logic (BSL) aufgenommen worden. Die Zeitschrift ist eine hervorragende Adresse für Forschungsarbeiten im Bereich Logik, und interessierte Wissenschaftlerinnen und Wissenschaftler sind herzlich eingeladen, Beiträge einzureichen: https://czasopisma.uni.lodz.pl/bulletin/index
</p><p>
Das Bulletin of the Section of Logic ist eine seit 1972 bestehende, fachlich begutachtete Fachzeitschrift, die von der Universität Łódź herausgegeben wird. Sie bietet ein internationales Forum für die schnelle Veröffentlichung wichtiger Ergebnisse in der Logik, insbesondere zu logischen Kalkülen, deren Methodik, Anwendungen und algebraischen Interpretationen.
|Beschreibung EN=Tim Lyon, who is a postdoctoral researcher at the ICCL, has joined the editorial board of the Bulletin of the Section of Logic (BSL). The journal is an excellent venue for research in logic, and researchers are warmly encouraged to submit their papers: https://czasopisma.uni.lodz.pl/bulletin/index
</p><p>
The Bulletin of the Section of Logic is a long-standing, peer-reviewed journal founded in 1972 and now published by the University of Łódź. It serves as an international forum for the rapid dissemination of significant results in logic, with a particular focus on logical calculi, their methodology, applications, and algebraic interpretations.
|URL=https://czasopisma.uni.lodz.pl/bulletin/index
|Datum=2026-01-13
|Forschungsgruppe=Computational Logic
}}

News109

2026-01-13T11:53:17Z

Tim Lyon: Die Seite wurde neu angelegt: „{{Neuigkeit |Titel DE=Tim Lyon ist dem Herausgebergremium des Bulletin of the Section of Logic beigetreten |Titel EN=Tim Lyon has joined the editorial board of the Bulletin of the Section of Logic |Beschreibung DE=Tim Lyon, Postdoktorand am ICCL, ist in das Herausgebergremium des Bulletin of the Section of Logic (BSL) aufgenommen worden. Die Zeitschrift ist eine hervorragende Adresse für Forschungsarbeiten im Bereich Logik, und interessierte Wissenschaft…“

{{Neuigkeit
|Titel DE=Tim Lyon ist dem Herausgebergremium des Bulletin of the Section of Logic beigetreten
|Titel EN=Tim Lyon has joined the editorial board of the Bulletin of the Section of Logic
|Beschreibung DE=Tim Lyon, Postdoktorand am ICCL, ist in das Herausgebergremium des Bulletin of the Section of Logic (BSL) aufgenommen worden. Die Zeitschrift ist eine hervorragende Adresse für Forschungsarbeiten im Bereich Logik, und interessierte Wissenschaftlerinnen und Wissenschaftler sind herzlich eingeladen, Beiträge einzureichen: https://czasopisma.uni.lodz.pl/bulletin/index

Das Bulletin of the Section of Logic ist eine seit 1972 bestehende, fachlich begutachtete Fachzeitschrift, die von der Universität Łódź herausgegeben wird. Sie bietet ein internationales Forum für die schnelle Veröffentlichung wichtiger Ergebnisse in der Logik, insbesondere zu logischen Kalkülen, deren Methodik, Anwendungen und algebraischen Interpretationen.
|Beschreibung EN=Tim Lyon, who is a postdoctoral researcher at the ICCL, has joined the editorial board of the Bulletin of the Section of Logic (BSL). The journal is an excellent venue for research in logic, and researchers are warmly encouraged to submit their papers: https://czasopisma.uni.lodz.pl/bulletin/index

The Bulletin of the Section of Logic is a long-standing, peer-reviewed journal founded in 1972 and now published by the University of Łódź. It serves as an international forum for the rapid dissemination of significant results in logic, with a particular focus on logical calculi, their methodology, applications, and algebraic interpretations.
|URL=https://czasopisma.uni.lodz.pl/bulletin/index
|Datum=2026-01-13
|Forschungsgruppe=Computational Logic
}}

Article3099

2026-01-11T15:19:17Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
|FurtherAuthors=Kees van Berkel
}}
{{Article
|Referiert=1
|Title=Proof Theory and Decision Procedures for Deontic STIT Logics
|To appear=0
|Year=2024
|Journal=Journal of Artificial Intelligence Research
|Volume=81
}}
{{Publikation Details
|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).
|Download=JAIR24-LyoBer.pdf
|Link=https://arxiv.org/abs/2402.03148
|DOI Name=https://doi.org/10.1613/jair.1.15710
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Inproceedings3402

2026-01-11T15:16:45Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
|FurtherAuthors=Ian Shillito; Alwen Tiu
}}
{{Inproceedings
|Referiert=1
|Title=Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
|To appear=0
|Year=2025
|Booktitle=Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic 2025
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik
|Editor=Jörg Endrullis, Sylvain Schmitz
|Series=LIPIcs
|Volume=326
}}
{{Publikation Details
|Abstract=It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott's existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.
|Download=2404.15855v3.pdf
|Link=https://arxiv.org/abs/2404.15855
|DOI Name=https://doi.org/10.4230/LIPIcs.CSL.2025.41
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Datei:2404.15855v3.pdf

2026-01-11T15:16:42Z

Tim Lyon:

Inproceedings3403

2026-01-11T15:16:12Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
}}
{{Inproceedings
|Referiert=1
|Title=Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
|To appear=0
|Year=2025
|Booktitle=Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic 2025
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik
|Editor=Jörg Endrullis, Sylvain Schmitz
|Series=LIPIcs
|Volume=326
}}
{{Publikation Details
|Abstract=We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini's sequent system GLseq, Shamkanov's non-wellfounded and cyclic sequent systems GL∞ and GLcirc, Poggiolesi's tree-hypersequent system CSGL, and Negri's labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GLseq, GL∞, and GLcirc, and Goré and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for Gödel-Löb provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GLseq and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GLseq, GL∞, GLcirc, CSGL, G3GL, and LNGL while also giving (to the best of the author's knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.
|Download=2410.24053v3 (2).pdf
|Link=https://arxiv.org/abs/2410.24053
|DOI Name=https://doi.org/10.4230/LIPIcs.CSL.2025.42
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Datei:2410.24053v3 (2).pdf

2026-01-11T15:16:09Z

Tim Lyon:

Inproceedings3404

2026-01-11T15:15:29Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
}}
{{Inproceedings
|Referiert=1
|Title=On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
|To appear=0
|Year=2025
|Booktitle=Proceedings of the Eleventh International Conference on Fundamentals of Software Engineering (FSEN)
|Pages=113-119
|Publisher=Springer
|Editor=Hossein Hojjat, Georgiana Caltais
|Series=LNCS
|Volume=15593
}}
{{Publikation Details
|Abstract=Propositional dynamic logic (PDL) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of PDL is solving fixed-point equations, i.e., formulae of the form x ≡ ϕ(x) such that x is a propositional variable and ϕ(x) is a formula containing x. A solution to such an equation is a formula ψ that omits x and satisfies ψ ≡ ϕ(ψ), where ϕ(ψ) is obtained by replacing all occurrences of x with ψ in ϕ(x). In this paper, we identify a novel class of PDL formulae arranged in two dual hierarchies for which every fixed-point equation x ≡ ϕ(x) has a solution. Moreover, we not only prove the existence of solutions for all such equations, but also provide an explicit solution ψ for each fixed-point equation.
|Download=2412.04012v1.pdf
|Link=https://arxiv.org/abs/2412.04012
|DOI Name=https://doi.org/10.1007/978-3-031-87054-5_8
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Datei:2412.04012v1.pdf

2026-01-11T15:15:26Z

Tim Lyon:

Article3103

2026-01-11T15:14:50Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
|FurtherAuthors=Agata Ciabattoni; Didier Galmiche; Marianna Girlando; Dominique Larchey-Wendling; Daniel Méry; Nicola Olivetti; Revantha Ramanayake
}}
{{Article
|Referiert=1
|Title=Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
|To appear=0
|Year=2025
|Journal=Bulletin of the Section of Logic
|Volume=54
|Number=1
|Pages=59–151
}}
{{Publikation Details
|Abstract=This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively easy while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi'. It is observed that these classes resist a rigorous separation, and we critically assess the properties that (calculi from) these classes are purported to possess.
<br>
Click on the link below for the arXiv version of the paper.
|Download=2312.03426v2.pdf
|Link=https://arxiv.org/abs/2312.03426
|DOI Name=10.18778/0138-0680.2025.02
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Datei:2312.03426v2.pdf

2026-01-11T15:14:48Z

Tim Lyon:

Inproceedings3402

2026-01-11T15:13:09Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
|FurtherAuthors=Ian Shillito; Alwen Tiu
}}
{{Inproceedings
|Referiert=1
|Title=Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
|To appear=0
|Year=2025
|Booktitle=Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic 2025
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik
|Editor=Jörg Endrullis, Sylvain Schmitz
|Series=LIPIcs
|Volume=326
}}
{{Publikation Details
|Abstract=It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott's existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.
|Link=https://arxiv.org/abs/2404.15855
|DOI Name=https://doi.org/10.4230/LIPIcs.CSL.2025.41
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Inproceedings3403

2026-01-11T15:12:43Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
}}
{{Inproceedings
|Referiert=1
|Title=Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
|To appear=0
|Year=2025
|Booktitle=Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic 2025
|Publisher=Schloss Dagstuhl - Leibniz-Zentrum für Informatik
|Editor=Jörg Endrullis, Sylvain Schmitz
|Series=LIPIcs
|Volume=326
}}
{{Publikation Details
|Abstract=We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini's sequent system GLseq, Shamkanov's non-wellfounded and cyclic sequent systems GL∞ and GLcirc, Poggiolesi's tree-hypersequent system CSGL, and Negri's labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GLseq, GL∞, and GLcirc, and Goré and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for Gödel-Löb provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GLseq and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GLseq, GL∞, GLcirc, CSGL, G3GL, and LNGL while also giving (to the best of the author's knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.
|Link=https://arxiv.org/abs/2410.24053
|DOI Name=https://doi.org/10.4230/LIPIcs.CSL.2025.42
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Article3103

2026-01-11T15:11:45Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Tim
|ErsterAutorNachname=Lyon
|FurtherAuthors=Agata Ciabattoni; Didier Galmiche; Marianna Girlando; Dominique Larchey-Wendling; Daniel Méry; Nicola Olivetti; Revantha Ramanayake
}}
{{Article
|Referiert=1
|Title=Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
|To appear=0
|Year=2025
|Journal=Bulletin of the Section of Logic
|Volume=54
|Number=1
|Pages=59–151
}}
{{Publikation Details
|Abstract=This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively easy while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi'. It is observed that these classes resist a rigorous separation, and we critically assess the properties that (calculi from) these classes are purported to possess.
<br>
Click on the link below for the arXiv version of the paper.
|Link=https://arxiv.org/abs/2312.03426
|DOI Name=10.18778/0138-0680.2025.02
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Beweistheorie
}}
{{Forschungsgebiet Auswahl
|Forschungsgebiet=Modal- und Temporallogiken
}}

Techreport3054

2026-01-11T15:10:03Z

Tim Lyon:

{{Publikation Erster Autor
|ErsterAutorVorname=Omar
|ErsterAutorNachname=Taher
|FurtherAuthors=Tim Lyon
}}
{{Techreport
|Title=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Year=2025
|Institution=TU Dresden
|Note=Report from Master's Project
}}
{{Publikation Details
|Abstract=This paper introduces an EXPTIME decision procedure for the (in)validity of Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
|Download=GL-Project .pdf
|Projekt=SECAI
|Forschungsgruppe=Computational Logic
}}

Techreport3054

2026-01-06T11:07:12Z

Tim Lyon: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Omar |ErsterAutorNachname=Taher |FurtherAuthors=Tim Lyon }} {{Techreport |Title=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents |Year=2025 |Institution=TU Dresden |Note=Report from Master's Project }} {{Publikation Details |Abstract=This paper introduces an EXPTIME decision procedure for the (in)validity of Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hyperseque…“

Datei:GL-Project .pdf

2026-01-06T11:06:55Z

Tim Lyon:

Datei:GL-Project download.pdf

2026-01-06T10:57:48Z

Tim Lyon:

Proof Theory and Sequent Systems (WS2025)

2025-12-18T13:46:02Z

Tim Lyon:

Proof Theory and Sequent Systems (WS2025)

2025-12-06T15:02:36Z

Tim Lyon:

Proof Theory and Sequent Systems (WS2025)

2025-11-21T08:03:05Z

Tim Lyon:

Proof Theory and Sequent Systems (WS2025)

2025-11-14T10:20:20Z

Tim Lyon:

Proof Theory and Sequent Systems (WS2025)

2025-11-10T11:51:53Z

Tim Lyon:

Proof Theory and Sequent Systems (WS2025)

2025-10-24T09:14:25Z

Tim Lyon:

Proof Theory and Sequent Systems (WS2025)

2025-10-07T11:21:13Z

Tim Lyon: Die Seite wurde neu angelegt: „{{Vorlesung |Title=Proof Theory and Sequent Systems |Research group=Computational Logic |Lecturers=Tim Lyon |Term=WS |Year=2025 |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…“

Thema3517

2025-09-02T12:25:10Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Titel EN=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Vorname=Omar
|Nachname=Y. A. A. Taher
|Abschlussarbeitstyp=Studienarbeit
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Abgeschlossen
|Beginn=2025-07-29
|Abgabe=2025-09-12
|Beschreibung DE=This paper introduces an EXPTIME decision procedure for the (in)validity of Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
|Beschreibung EN=This paper introduces an EXPTIME decision procedure for the (in)validity of Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
}}

Datei:GL-Project.pdf

2025-09-02T12:25:07Z

Tim Lyon: Tim Lyon lud eine neue Version von Datei:GL-Project.pdf hoch

Thema3517

2025-09-02T12:23:46Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Titel EN=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Vorname=Omar
|Nachname=Y. A. A. Taher
|Abschlussarbeitstyp=Studienarbeit
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Abgeschlossen
|Beginn=2025-07-29
|Abgabe=2025-09-12
|Ergebnisse=GL-Project.pdf
|Beschreibung DE=This paper introduces an EXPTIME decision procedure for the (in)validity of Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
|Beschreibung EN=This paper introduces an EXPTIME decision procedure for the (in)validity of Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
}}

Datei:GL-Project.pdf

2025-09-02T12:22:15Z

Tim Lyon: Tim Lyon lud eine neue Version von Datei:GL-Project.pdf hoch

Thema3517

2025-09-02T12:20:19Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Titel EN=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Vorname=Omar
|Nachname=Y. A. A. Taher
|Abschlussarbeitstyp=Studienarbeit
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Abgeschlossen
|Beginn=2025-07-29
|Abgabe=2025-09-12
|Ergebnisse=GL-Project.pdf
|Beschreibung DE=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
|Beschreibung EN=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
}}

Thema3517

2025-09-02T12:20:01Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Titel EN=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Vorname=Omar
|Nachname=Y. A. A. Taher
|Abschlussarbeitstyp=Studienarbeit
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Abgeschlossen
|Beginn=2025-07-29
|Abgabe=2025-09-12
|Ergebnisse=GL-Project.pdf
|Beschreibung DE=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
|Beschreibung EN=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
}}

Thema3517

2025-09-02T12:11:00Z

Tim Lyon:

{{Abschlussarbeit
|Titel DE=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Titel EN=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Vorname=Omar
|Nachname=Y. A. A. Taher
|Abschlussarbeitstyp=Studienarbeit
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Abgeschlossen
|Beginn=2025-07-29
|Abgabe=2025-09-12
|Ergebnisse=GL-Project.pdf
|Beschreibung DE=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
|Beschreibung EN=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
}}

Thema3517

2025-09-02T12:08:53Z

Tim Lyon: Die Seite wurde neu angelegt: „{{Abschlussarbeit |Titel DE=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents |Titel EN=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents |Vorname=Omar |Nachname=Y. A. A. Taher |Abschlussarbeitstyp=Studienarbeit |Betreuer=Tim Lyon |Forschungsgruppe=Computational Logic |Abschlussarbeitsstatus=Abgeschlossen |Beschreibung DE=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-L…“

{{Abschlussarbeit
|Titel DE=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Titel EN=Automated Proof-Search for Gödel-Löb Provability Logic via Tree Sequents
|Vorname=Omar
|Nachname=Y. A. A. Taher
|Abschlussarbeitstyp=Studienarbeit
|Betreuer=Tim Lyon
|Forschungsgruppe=Computational Logic
|Abschlussarbeitsstatus=Abgeschlossen
|Beschreibung DE=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
|Beschreibung EN=This paper introduces an EXPTIME decision procedure for (in)validity for the Gödel-Löb Provability Logic via a syntactic variant of the Tree-Hypersequent System CSGL.
}}

Datei:GL-Project.pdf

2025-09-02T12:06:30Z

Tim Lyon: