Beweistheorie

Die Beweistheorie beschäftigt sich mit den formalen Eigenschaften und Anwendungsmöglichkeiten mathematischer Beweise. Damit dient sie als eine der tragenden Säulen der mathematischen Logik. Typischerweise werden Beweise als syntaktische Objekte definiert, die induktiv durch Anwendungen von Inferenzregeln auf eine Menge von Annahmen, Axiomen oder im Vorfeld geführten Beweisen, konstruiert werden können. Da Beweise durch das Manipulieren von Formeln und Symbolen durch Inferenzregeln konstruiert werden, ist die Beweistheorie ihrem Wesen nach syntaktisch. Daher sind Beweiskalküle für logisches Schließen im Bereich der Informatik bestens geeignet. In diesem Kontext hat sich die Beweistheorie als effektives Werkzeug im automated reasoning herausgestellt, das es erlaubt, Entscheidungsverfahren zu entwickeln, welche optimal hinsichtlich ihrer Komplexitätseigenschaften sind und sogenannte verifiable witnesses für (un)erfüllbare logische Aussagen bereitstellen. Auf theoretischer Ebene erlauben es Techniken aus der Beweistheorie beispielsweise die Konsistenz, Entscheidbarkeit oder Interpolierbarkeit von Logiken sowie weitere signifikante Eigenschaften zu zeigen.
Typische Fragestellungen der Beweistheorie sind: Was ist ein mathematischer Beweis? Wie können Beweiskalküle konstruiert werden, sodass sie für automated reasoning geeignet sind? Wie könnte ein Beweiskalkül aufgebaut sein, bei dem alle Beweise analytischer Natur sind (d.h. alle im Beweis verwendeten Informationen sind in der Konklusion des Beweises vorhanden)?

Wissenschaftliche Mitarbeiter

Dr. Tim Lyon

Computational Logic

Artikel in Fachzeitschriften

Bartosz Bednarczyk, Sebastian Rudolph
How to Tell Easy from Hard: Complexities of Conjunctive Query Entailment in Extensions of ALC
Journal of Artificial Intelligence Research, 78:385–458, November 2023
Details Download

Tim Lyon
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
Journal of Applied Non-Classical Logics, 33(2):121-164, 2023
Details

Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, Alwen Tiu
Display to Labeled Proofs and Back Again for Tense Logics
ACM Transactions on Computational Logic, 22(3):1-31, August 2021
Details Download

Tim Lyon
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
Journal of Logic and Computation, 31(1):213-265, 2021
Details Download

Tim Lyon, Christian Ittner, Timo Eckhardt, Norbert Gratzl
The Basics of Display Calculi
Kriterion -- Journal of Philosophy, 31(2):55-100, 2017
Details Download

Artikel in Tagungsbänden

Tim Lyon, Jonas Karge
Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
Proceedings of the 33rd International Joint Conference on Artificial Intelligence, IJCAI 2024, to appear. ijcai.org
Details Download

Tim Lyon, Piotr Ostropolski-Nalewaja
Connecting Proof Theory and Knowledge Representation: Sequent Calculi and the Chase with Existential Rules
Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, 769-773, 2023. IJCAI Inc
Details Download

Bartosz Bednarczyk, Reijo Jaakkola
Towards Model Theory of Ordered Logics: Expressivity and Interpolation
In Stefan Szeider, Robert Ganian, Alexandra Silva, eds., Proceedings of the 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), volume 241 of Leibniz International Proceedings in Informatics, 15:1--15:14, August 2022. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
Details Download

Tim Lyon, Jonas Karge
Uniform and Modular Sequent Systems for Description Logics
In Ofer Arieli, Martin Homola, Jean Christoph Jung, Marie-Laure Mugnier, eds., Proceedings of the 35th International Workshop on Description Logics (DL 2022), 2022
Details Download

Tim Lyon
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
In Anupam Das, Sara Negri, eds., Automated Reasoning with Analytic Tableaux and Related Methods, 409-427, August 2021. Springer International Publishing
Details Download

Tim Lyon
A Framework for Intuitionistic Grammar Logics
In Pietro Baroni, Christoph Benzmüller, Yὶ N. Wang, eds., Logic and Argumentation, volume 13040, 495-503, October 2021. Springer International Publishing
Details Download

Kees van Berkel, Tim Lyon
The Varieties of Ought-implies-Can and Deontic STIT Logic
In Fenrong Liu, Alessandra Marra, Paul Portner and Frederik Van De Putte, eds., Deontic Logic and Normative Systems: 15th International Conference, DEON 2020/2021, 57-76, July 2021. College Publications
Details Download

Tim Lyon, Alwen Tiu, Rajeev Goré, Ranald Clouston
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
In Maribel Fernández and Anca Muscholl, eds., 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152, 28:1--28:16, 2020. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Details Download

Tim Lyon, Kees van Berkel
Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
In Baldoni, Matteo and Dastani, Mehdi and Liao, Beishui and Sakurai, Yuko and Zalila Wenkstern, Rym, eds., PRIMA 2019: Principles and Practice of Multi-Agent Systems, volume 11873, 202-218, 2019. Springer
Details Download

Kees van Berkel, Tim Lyon
Cut-Free Calculi and Relational Semantics for Temporal STIT Logics
In Calimeri, Francesco and Leone, Nicola and Manna, Marco, eds., Logics in Artificial Intelligence, volume 11468, 803-819, 2019. Springer
Details Download

Tim Lyon, Agata Ciabattoni, Revantha Ramanayake
From Display to Labelled Proofs for Tense Logics
In Artemov, Sergei and Nerode, Anil, eds., From Display to Labelled Proofs for Tense Logics, volume 10703, 120-139, 2018. Springer International Publishing
Details Download

Dissertationen

Tim Lyon
Refining Labelled Systems for Modal and Constructive Logics with Applications
Phd thesis, Technische Universität Wien, 2021/07/29
Details