Beweistheorie

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

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)?

Artikel in Fachzeitschriften

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, 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
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