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 email, please subscribe to the
mailing list of this seminar on its
administration page.
Preliminary Programme
Archive
 June 19, 2024

Johanne Müller Vistisen
title: NPcompleteness of the Smallest 1Level Grammar Problem
abstract:
The Smallest 1Level Grammar Problem focuses on identifying the most compact
1level grammar capable of generating a given string, a challenge which is
relevant in many research areas in need of spaceefficient string compression.
A 1level grammar is one where every nonterminal except the start symbol has a
production rule that directly results in terminal strings. It was a long time
open question whether the Smallest Grammar Problem was NPhard, and initial
proofs were limited to cases involving infinite alphabets. This paper examines
the complexity of the Smallest 1Level Grammar Problem for a finite alphabet.
By reducing the wellknown Vertex Cover Problem to the Smallest 1Level Grammar
Problem, we demonstrate its NPhardness even for an alphabet of size five.
 June 5, 2024

Vittorio Cipriani
title: On the computational complexity of unfriendly partitions
abstract:
In this talk, the graphs G = (V,E) we consider are countable,
undirected, and without selfloops. A partition V(G)= V_{0} ∪ V_{1}
of the
vertices of a graph G is unfriendly if every vertex in V_{0} has more
(or equal number) of neighbors in the opposite partition than in its one. Cowan
and Emerson conjectured that every graph has an unfriendly partition, but
Milner and Shelah provided a counterexample. However, the graph they exhibit as
a counterexample is an uncountable one, therefore, the conjecture remains open
for the countable case. It is known that such a conjecture is true for certain
classes of graphs: To show these results, different proof techniques have been
used. In this talk, we address the problem of how complicated it is to find
unfriendly partitions of a graph from a computability perspective. This talk
collects preliminary results from joint work with Belanger, Goh, and Stephan.
 May 22, 2024

Alexander Leitsch
title: FirstOrder Schemata and Herbrand's theorem
abstract:
Proofs are more than just validations of theorems; they can contain interesting
mathematical information like bounds or algorithms. However this information is
frequently hidden and proof transformations are required to make it explicit.
One such transformation on proofs in sequent calculus is cutelimination (i.e.
the removal of lemmas in formal proofs to obtain proofs made essentially of the
syntactic material of the theorem). In his famous paper "Untersuchungen ueber
das logische Schliessen" Gentzen showed that for cutfree proofs of prenex
endsequents Herbrand's theorem can be realized via the midsequent theorem. In
fact Gentzen defined a transformation which, given a cutfree proof p of a
prenex sequent S, constructs a cutfree proof p' of a sequent S' (a socalled
Herbrand sequent) which is propositionally valid and is obtained by
instantiating the quantifiers in S. These instantiations may contain
interesting and compact information on the validity of S. Generally, the
construction of Herbrand sequents requires cutelimination in a given proof p
(or at least the elimination of quantified cuts). The method CERES
(cutelimination by resolution) provides an algorithmic tool to compute a
Herbrand sequent S' from a proof p (with cuts) of S even without constructing a
cutfree version of p.
A prominent and crucial principle in mathematical proofs
is mathematical induction. However, in proofs with mathematical induction
Herbrand's theorem typically fails. To overcome this problem we replace
induction by recursive definitions and proofs by proof schemata and define a
schematic CERESmethod CERESs. While schematic representations of Herbrand
substitutions defining infinite sequences of Herbrand sequents (so called
Herbrand systems) could not be computed in the original method CERESs, a
recent development of a more powerful schematic refutational (resolution)
calculus solves this problem. We present in detail how Herbrand schemata can be
extracted from refutations of formula schemata in the new calculus, which forms
the central step in CERESs. In a final step the Herbrand systems of the
projection schemata and of the refutation schemata have to be combined to
obtain a Herbrand schema for the original proof.
 May 15, 2024

Dino Rossegger
title: Feferman's completeness theorem  revisited
abstract:
In 1962, Feferman showed that any arithmetical theorem is a consequence
of a transfinite iteration of uniform reflection (a consistency
progression) of Peano arithmetic along a suitable ordinal notation.
While this result provides substantial insight into the nature of
arithmetical theorems  it shows that uniform reflection does not provide
a suitable measure for their prooftheoretic strength  it is mysterious
and often overlooked.
In upcoming work with Fedor Pakhomov and Michael Rathjen, we revisit
this old theorem and give three new proofs: One simple, using wellknown
results in computability theory and secondorder arithmetic. An
adaptation of the first proof integrates results of Ash and Knight from
computable structure theory to obtain exact bounds on the order types of
the involved ordinal notations and, at last, a proof using
prooftheoretic tools that emerged at the time of Feferman's result.
In my talk, I will give the easy proof of Feferman's completeness
theorem from first principles and sketch the modifications that allow us
to obtain exact bounds.
 May 8, 2024

Martin Ritter
title: Learning of c.e. sets up to equivalence relations
abstract:
We report on an ongoing project which aims to generalize the classic framework
for learning computably enumerable (c.e.) sets from text, by allowing the
learner to stabilize to a conjecture which is "sufficiently similar" to the
observed set. In a nutshell, our learners output indices of c.e. sets and
they are required to stabilize to a guess that is correct up to a suitable
equivalence relation on the c.e. sets. This perspective extends the scope of
the socalled anomalous learning. We offer a characterization of which
equivalence relations are universal (in the sense, that they allow to learn all
families of c.e. sets) for the case of Bclearning (behaviorally
correct). We also prove that there is an equivalence relation that is
Bcuniversal but not Exuniversal (explanatory). This is
joint work with Vittorio Cipriani and Luca San Mauro.
 April 10, 2024

Fabian Wöhrer
title: Reversible Automata: Characterizations and Construction
abstract:
A finite automaton is called reversible, if every letter induces a partial injective map from the set of states into itself. We will characterize the corresponding class of reversible languages from a grouptheoretic, algebraic and topological perspective.
Afterwards we solve the membership problem algorithmically and present a procedure that transforms the minimal DFA of a reversible language into an equivalent reversible automaton.
 March 20, 2024

Florian Grünstäudl
title: Beth's Definability Theorem and the Complexity of Explicit Definitions
abstract:
We will briefly discuss the proof of Beth's Definability Theorem for first order logic.
The main part of the presentation will be dedicated to Friedman's proof of the fact that the
quantifier complexity of the explicit definitions obtained by Beth's Theorem is not computable.
 March 13, 2024

Johannes Weiser
title: Complexity Bounds for CutElimination
abstract:
It is wellknown that cutelimination in firstorder logic is nonelementary.
In this work we analyse the height of the tower of exponentials for bounds
related to cutelimination.
We take up a suggestion by S. Buss that it should be possible to obtain an
upper bound on the length of the cutfree proof in terms of d+1 iterations of
the exponential function where d is the number of quantifer alternations in the
cut formulas of the original proof. We show this result by combining Buss' work
with a result by Weller on the elimination of quantifierfree cuts.
Last Change: 20240620, Stefan Hetzl