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
seminar room DC red 07.
The seminar is organised by
J. Aguilera,
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
- November 4, 2026
-
Logan McDonald (TU Wien)
title: Mass Problems and Cardinal Characteristics
abstract:
Effective analogues of objects studied in set theory often yield rich
structures in computability. The families that witness various cardinal
characteristics (MAD families, maximal towers, ultrafilter bases, etc.) can be
studied in computability by restricting to only computable reals in their
definitions. In the effective setting, these families must be countable and can
be coded by a single real. The hope is that when we can prove an inequality
between cardinal characteristics in set theory, we can find a similar relation
in terms of the complexities of these analogues.
- November 11, 2026
-
Elijah Schulzki (TU Wien)
title: t.b.a.
Archive
- October 28, 2026
-
Antonio Nakid Cordero (TU Wien)
title: Martin's Conjecture in the Enumeration Degrees
abstract:
Informally, Martin's Conjecture asserts that every definable function on the
Turing degrees is, on a cone, either constant or an iterate of the Turing jump.
This classification has already been proven for the uniformly invariant
functions and a long-standing conjecture by Steel is that every definable
function on the Turing degrees is equivalent on a cone to a uniformly invariant
one.
The Turing degrees embed into the enumeration degrees and the Turing jump has
two natural extensions: the enumeration jump and the skip. We explore whether a
similar classification holds in this setting. We show that even the uniformly
invariant functions exhibit a much wider spectrum of global behavior. Still,
our main result is a sharp local classification: restricted to (the elements
of) a single degree, a uniformly invariant function is constant, increasing or
above the skip. As a consequence, we construct a definable function in the
enumeration degrees that is not equivalent to a uniformly invariant one on any
cone, refuting the analogue of Steel's conjecture.
- October 14, 2026
-
Franziskus Wiesnet (TU Wien)
title: On the Limits of Recursive Characterizations in the Refined A-Translation
abstract:
The refined A-translation, due to Berger, Buchholz, and Schwichtenberg, is based on recursively defined classes of formulas in minimal arithmetic, in particular the classes of definite and goal formulas. Schwichtenberg and Wainer observed that one of the key proof-theoretic properties of definite formulas also holds for formulas outside the original class and asked whether all formulas satisfying this property admit a useful characterization.
In this talk, I show that this is not possible. More precisely, none of the four proof-theoretic properties associated with the formula classes in the refined A-translation admits a recursive characterization. We will also show how the original framework can nevertheless be extended, and present an extended formulation of the refined A-translation including conjunction.
- October 7, 2026
-
Johannes Weiser (TU Wien)
title: Comparing Explicit and Implicit Methods for Solving CHCs
abstract:
Constrained Horn Clauses (CHCs) can be considered to be an intermediate
representation language of (recursive) computer programs and assertions about
them. Similar to programs, they can be executed symbolically. In this talk, we
present algorithms for symbolically executing CHCs in both forward and backward
direction. These are implicit methods since they do not produce an explicit
invariant of the system. We show how to construct an explicit invariant after
either symbolic execution algorithm terminates, even in the case of nonlinear
clauses. We compare our algorithms with explicit methods that produce
invariants. We show that all of these methods (forward execution, backward
execution, searching for explicit quantifier-free invariants) are pairwise
incomparable.
- September 23, 2026
-
Anders Lundstedt (Stockholm University)
title: Finitely non-standard models of Robinson arithmetic
abstract:
To the best of my knowledge, there is no systematic study of *finitely
non-standard* models of Robinson arithmetic - that is, there is no systematic
study of those models of Robinson arithmetic that have a non-empty finite set
of non-standard numbers. I will present a modest attempt at such a systematic
study. With addition and multiplication both defined recursively in the second
argument, the main conclusions are roughly: (1) addition and multiplication
with a non-standard first argument is "well-behaved"; and (2) addition and
multiplication with a non-standard second argument is "wild".
- September 16, 2026
-
Heer Tern Koh (University of Electronic Science and Technology of China)
title: (Non-)density of punctual degrees
abstract:
A punctual structure is a countable structure with domain omega whose functions
and relations are uniformly primitive recursive. Since the inverse of a
bijective primitive recursive function is not necessarily primitive recursive,
the relation "being primitive recursively isomorphic" is a preorder rather than
an equivalence relation. This gives rise to a degree structure which we call
the punctual degrees. Intuitively, this is an algorithmic invariant which
measures the different primitive recursive speeds of enumerations of a given
(punctual) structure. In this talk, we provide a survey of results and
techniques concerning density and non-density of the punctual degrees of
various structures.
Last Change: 2026-11-02, Stefan Hetzl.