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
"Dissertantenraum" in Freihaus, 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
Archive
- June 19, 2024
-
Johanne Müller Vistisen
title: NP-completeness of the Smallest 1-Level Grammar Problem
abstract:
The Smallest 1-Level Grammar Problem focuses on identifying the most compact
1-level grammar capable of generating a given string, a challenge which is
relevant in many research areas in need of space-efficient string compression.
A 1-level 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 NP-hard, and initial
proofs were limited to cases involving infinite alphabets. This paper examines
the complexity of the Smallest 1-Level Grammar Problem for a finite alphabet.
By reducing the well-known Vertex Cover Problem to the Smallest 1-Level Grammar
Problem, we demonstrate its NP-hardness 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 self-loops. A partition V(G)= V0 ∪ V1
of the
vertices of a graph G is unfriendly if every vertex in V0 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: First-Order 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 cut-elimination (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 cut-free proofs of prenex
end-sequents Herbrand's theorem can be realized via the midsequent theorem. In
fact Gentzen defined a transformation which, given a cut-free proof p of a
prenex sequent S, constructs a cut-free proof p' of a sequent S' (a so-called
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 cut-elimination in a given proof p
(or at least the elimination of quantified cuts). The method CERES
(cut-elimination by resolution) provides an algorithmic tool to compute a
Herbrand sequent S' from a proof p (with cuts) of S even without constructing a
cut-free 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 CERES-method CERES-s. While schematic representations of Herbrand
substitutions defining infinite sequences of Herbrand sequents (so called
Herbrand systems) could not be computed in the original method CERES-s, 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 proof-theoretic 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 well-known
results in computability theory and second-order 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
proof-theoretic 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 so-called 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 Bc-learning (behaviorally
correct). We also prove that there is an equivalence relation that is
Bc-universal but not Ex-universal (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 group-theoretic, 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 Cut-Elimination
abstract:
It is well-known that cut-elimination in first-order logic is non-elementary.
In this work we analyse the height of the tower of exponentials for bounds
related to cut-elimination.
We take up a suggestion by S. Buss that it should be possible to obtain an
upper bound on the length of the cut-free 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 quantifier-free cuts.
Last Change: 2024-06-20, Stefan Hetzl