Computational Logic Seminar


General Information

This is the website of the research seminar of the Computational Logic Group at the Institute of Discrete Mathematics and Geometry of TU Wien. The seminar usually takes places on Wednesdays from 10:00 to 11:00 in the Zeichensaal 1, 8th floor, green area. The seminar is organised by E. Fokina and S. Hetzl.

If you want to receive talk announcements by e-mail, please subscribe to the mailing list of this seminar on its administration page.

Preliminary Programme

April 2, 2025
Hanul Jeon (Cornell, TU Wien)
title: Dilators in descriptive set theory
abstract:
In this introductory talk, I will introduce dilators and how a Suslin representation of $\Pi^1_1$ and $\Sigma^1_2$ sets is related to dilators. Most results in this talk are well-known.
April 9, 2025
Raphael Gruber (TU Wien)
title: t.b.a.
April 30, 2025
Franziskus Wiesnet (TU Wien)
title: Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Friends
May 7, 2025
Matthias Baaz (TU Wien)
title: t.b.a.

Archive

March 26, 2025
Bahareh Afshari (University of Gothenburg)
title: Cyclic Proof Theory
abstract: Proofs are a central tool in mathematics and a core concept in the study of formal reasoning. Traditionally, a proof is conceived as a finite object which is used to certify the correctness of our mathematical structures and their properties. Less common are so called cyclic proofs which, although infinitary, exhibit periodic patterns. Cyclic proof systems have proven to be a remarkably useful alternative in the mathematical study of computational systems, particularly in connection with algorithms, databases and programs. In this talk we will introduce cyclic proofs and study the extent to which these classes of proofs lend themselves to traditional proof theoretic techniques.
March 19, 2025
Miguel Aguilar (TU Wien)
title: The Mountain Pass Theorem in Subsystems of Second Order Arithmetic
abstract:
The main goal of this talk is to show a formalized proof of the Mountain Pass Theorem of Ambrosetti and Rabinowitz within the formal subsystem of second order arithmetic known as ACA0. We develop some Analysis within this system to have access to the space of continuous functions from [0,1] into a separable Banach space and from there we built formalized proofs of the basic ingredients of the Mountain Pass Theorem: The deformation lemma (for which a good deal of the theory of ODEs is needed) and the minimax principle that proves the theorem itself.
March 12, 2025
Ellen Hammat (TU Wien)
title: Arriving on time: punctuality in structures and isomorphisms
abstract:
In this talk we investigate what happens when we take concepts from computable structure theory and forbid the use of unbounded search. In other words, we discuss the primitive recursive content of computable structure theory. The central definition is that of punctual structures, introduced by Kalimullin, Melnikov and Ng in 2017. A common theme is that new techniques are required in the primitive recursive analogue of computable structure theory concepts. We also discuss a degree structure within punctual presentations which is induced by primitive recursive isomorphisms. This degree structure is a new concept that does not arise in computable structure theory.
March 5, 2025
Manuel Schweigler (TU Wien)
title: Proof Systems for Regular Expressions
abstract:
We are interested in proving equations between regular expressions by applying substitutions defined by a set of axioms. The key insight of this thesis is that there exists no finite axiom system that can be used to prove all valid equations. To show this, we assume there exists such a finite proof system. By generalizing this system to a certain axiomatization, we can construct an equation that cannot be derived by this system.
Furthermore, we introduce two alternative proof systems that implement a finite axiomatization by introducing special transformations. Lastly, we analyze the complexity of proving the equality of regular expressions.

Archive (winter term 2024/25)

Archive (summer term 2024)

Archive (winter term 2023/24)

Archive (summer term 2023)


Last Change: 2025-04-01, Stefan Hetzl.