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 30, 2025
-
Franziskus Wiesnet (TU Wien)
title: Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Friends
abstract:
We present Minlog and the theory of program extraction from constructive
proofs, through the constructive formalization of central theorems in
elementary number theory.
Formalizing proofs in Minlog ensures not only their correctness, but also
allows for the automatic extraction of executable programs. To achieve
efficient implementations, algorithmic considerations are already incorporated
during the proof development. For example, we use the binary representation of
natural numbers, which is much more efficient for computation than the
traditional unary (successor-based) encoding.
Our formalization includes results such as Bézout's identity, the Fundamental
Theorem of Arithmetic, and Fermat's factorization method. Through selected
examples, we will show how the constructive and algorithmically approach
influences the structure of the proofs and how it differs from standard proofs.
Some of the extracted programs will be presented in Haskell.
No prior knowledge of Minlog or formal logic is required. A basic understanding
of elementary number theory will be sufficient to follow the talk.
- May 7, 2025
-
Matthias Baaz (TU Wien)
title: t.b.a.
Archive
- April 9, 2025
-
Raphael Gruber (TU Wien)
title: Boolean Equations
abstract:
We study equations with unknowns in an arbitrary Boolean algebra and their
solution theory, as presented in [Rudeanu, 1974]. We highlight conditions for
the existence of solutions to such equations and methods to compute them.
(method of successive eliminations and Löwenheim's theorem). This theory can
be seen as a generalisation of the SAT problem, as the satisfiability of a
given Boolean formula can be reformulated into a Boolean equation in the
two-element Boolean algebra.
- 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.
- 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-16, Stefan Hetzl.