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 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
- January 15, 2025
-
Tobias Leichtfried (TU Wien)
title: t.b.a.
- January 22, 2025
-
t.b.a.
title: t.b.a.
- January 29, 2025
-
Raphael Gruber (TU Wien)
title: t.b.a.
Archive
- December 18, 2024
-
Franziskus Wiesnet (TU Wien)
title: Material Interpretation and Constructive Analysis of Maximal Ideals in ℤ[X]
abstract:
We explore the constructive characterization of all maximal ideals in ℤ[X],
which serves as a case study for the concept of the "Material Interpretation".
Starting with a classical proof, we demonstrate how it can be transformed into
a constructive proof, potentially leading to stronger statements. The Material
Interpretation provides an alternative proof interpretation, transforming
statements of the form A → B into ¬A ∨ B, where ¬A represents a constructively
stronger form of the negation of A. We will discuss the theoretical foundations
of this approach as well as its formalization as Python program and in some
proof assistance such as Agda and Lean, which is still a work in progress.
Finally we will show further applications and discuss future work on the
material interpretation.
- December 11, 2024
-
Dino Rossegger (TU Wien)
title: On the descriptive complexity of equivalence relations arising in model theory
abstract:
In this talk we survey various results shedding light on the complexity of equivalence relations arising
in countable model theory. We will see that the elementary embeddability quasi-order on countable
graphs and its associated equivalence relation, elementary bi-embeddability, are analytic complete
with respect to Borel reducibility, that the Borel complexity of the models of a first-order theory is
partially characterized by the quantifier complexity of its optimal first-order axiomatization, and
study the complexity of the isomorphism relation on linear orderings and models of Peano arithmetic
via a rigorous Scott analysis. Additionally we will mention connections to algorithmic properties of these equivalence relations.
( Vorstellungsvortrag von Hrn. Dino Rossegger - Habilitationswerber an der
Fakultät für Mathematik und Geoinformation, angestrebtes
Habilitationsfach: "Mathematik" )
- November 6, 2024
-
Liling Ko (TU Wien)
title: Chip-firing on countably-infinite graphs
abstract:
Chip-firing is a single-player game played on an undirected graph. Each vertex of the graph contains some natural number of chips. If the vertex has more chips than neighbors, it can be played by sending one chip to each neighbor, changing the distribution of chips on the graph. The game is typically played on finite graphs. We study this game in an infinite setting, allowing graphs to be countable with complex structure. We investigate variants of the game that are meaningful in the infinite setting and study the computational complexities of winning strategies on computable graphs. We also consider the computational complexities of determining which chip distributions are achievable.
This work is joint with David Belanger, Damir Dzhafarov, Justin Miller, and Reed Solomon.
- October 23, 2024
-
Leonardo Pacheco (TU Wien)
title: Feedback computation and reflecting ordinals
abstract:
Feedback Turing machines are Turing machines which can query a halting oracle which has information on the convergence or divergence of feedback computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze?
We define \alpha-th order feedback Turing machines for each computable ordinal \alpha. We first describe feedback computable sets using inductive definitions. We also briefly comment on the relation between feedback computable sets and Gale-Stewart games. At last, we describe feedback computable sets using the \alpha-reflecting ordinals of Lubarsky.
This is joint work with Juan P. Aguilera and Robert S. Lubarsky. Some of the results I will talk about are in the paper "Higher-Order Feedback Computation" (https://doi.org/10.1007/978-3-031-64309-5_24).
- October 16, 2024
-
David Cerna (CAS ICS)
title: One is all you need: Second-order Unification without First-order Variables
abstract:
We introduce a fragment of second-order unification, referred to as
Second-Order Ground Unification (SOGU), with the following properties: (i) only
one second-order variable is allowed, and (ii) first-order variables do not
occur. We study an equational variant of SOGU where the signature contains
associative binary function symbols (ASOGU) and show that Hilbert's 10th
problem is reducible to ASOGU unifiability, thus proving undecidability. Our
reduction provides a new lower bound for the undecidability of second-order
unification, as previous results required first-order variable occurrences,
multiple second-order variables, and/or equational theories involving
length-reducing rewrite systems. Furthermore, our reduction holds even in the
case when associativity of the binary function symbol is restricted to power
associative, i.e. f(f(x,x),x)= f(x,f(x,x)), as our construction requires a
single constant.
- October 11, 2024, 13:00 - 14:00, Zeichensaal 1
-
Jan von Plato (Helsinki)
title: On normal derivability in Gödel-Löb logic
abstract:
Gigi Bellin published
in 1985 a proof of normalization for a system of natural deduction
for the Gödel-Löb provability logic GL, but his very involved proof
seems to have remained unread. A clear and simple proof of
normalization is given, the crux of which is a conversion algorithm
that reduces several instances of the modal rule with the same
diagonal formula into one.
- October 2, 2024
-
Johannes Weiser (TU Wien)
title: Subsystems of Open Induction
abstract:
It was shown that open induction often constitutes an upper bound as to what
automated theorem provers can prove. In this presentation, we will consider
subsystems of open induction over inductive datatypes. In particular, we will
deal with arithmetics, lists and general inductive datatypes. We will give
examples of when there is an alternative axiomatization of open induction and
when open induction collapses to a lower level (e.g. induction over literals).
Last Change: 2024-12-18, Stefan Hetzl.