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
Archive
- 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-11-18, Stefan Hetzl.