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.
Last Change: 2025-04-01, Stefan Hetzl.