#### Talks during the fall term 2018

Wed 5.9.2018 12-14, C124**Dependence logic minisymposium**

12.15 Juha Kontinen: First-order definable team properties

12.40 Fan Yang: Union closed logics: axiomatizations and expressive power

13.05 Break

13.10 Miika Hannula: Automated reasoning about key sets

13.35 Vadim Kulikov: Probabilistic team semantics

Wed 12.9.2018 12-14, C124

Jouko Väänänen: Team semantics of anonymity

Wed 19.9.2018 **Extra guest seminar: 10-11 in C123** Natasha Dobrinen: Ramsey theory of the universal homogeneous triangle-free graph

12-14, C124 Kaisa Kangas: An AEC framework for fields with commuting automorphisms

Wed 26.9.2018 12-14, C124

Åsa Hirvonen: On metric variants of dependence/independence atoms

Wed 3.10.2018 12-14, C124

cancelled

Wed 10.10.2018 12-14, C124

Karoliina Lehtinen: Quasi-polynomial solutions for parity games and other problems

Abstract:

Parity games are infinite two-player games, which are used in verification, automata theory, and reactive synthesis. Solving parity games -- that is, deciding which player has a winning strategy -- is one of the few problems known to be in both UP and co-UP yet not known to be in P. So far, the quest for a polynomial algorithm has lasted over 25 years. Last year, a major breakthrough occurred: parity games are solvable in quasi-polynomial time.

From an automata-perspective, solving parity games can be done by transforming alternating parity word automata into alternating weak automata. From a logician's perspective, solving parity games can be done by finding a mu-calculus formula that recognises the winning region of a player in the parity game. Then, the size blow-up of the automaton in the first case, and the complexity of the formula in the second case, determine the complexity of the consequent algorithm for solving parity games.

In this talk, I present a quasi-polynomial solution for all three problems, based on playing parameterised games on parity-game arenas.

This talk is based on "A modal mu perspective on solving parity games in quasi-polynomial time", presented at LICS'18 and "On the way to alternating weak automata" (co-authored with Udi Boker) to appear at FSTTCS'18.

Wed 17.10.2018 12-14, C124

Fausto Barbero: Regular and irregular fragments of IF logic

Abstract:

I will present some joint work developed with L.Hella and R.Rönnholm in the proceedings paper "Independence-friendly logic without Henkin quantification", and some further results, concerning the expressive power and complexity of some fragments of IF logic. The kind of fragments which are considered are picked, mostly, according to game-theoretical considerations.

First, I will show how the signalling quantifier prefixes can be used to simulate Henkin quantifiers of arbitrarily large Krynicki normal form; this proves that the regular, prenex fragment of action recall has full ESO expressivity. Similar (but simpler) results can be obtained for appropriate regular, non-prenex fragments of action recall without signalling sequences; here the source of expressivity is "signalling by disjunction." In the second half of the talk I will present some peculiarities of irregular quantifier prefixes and fragments (where requantification is allowed), including an extension of the knowledge memory theorem to the irregular case.

Wed 24.10.2018 12-14, C124

exam week

Wed 31.10.2018 12-14, C124

Chinese-Finnish Logic Workshop

Wed 7.11.2018 12-14, C124

Heikki Tuuri: How does destructive interference work in quantum mechanics

Wed 14.11.2018 12-14, C124

Miika Hannula: Probabilistic dependencies

Wed 21.11.2018 12-14, C124

Martin Lück: The Complexity of Modal Team Logic and First-Order Team Logic

Abstract: Modal team logic (MTL) is the smallest extension of modal logic with team semantics closed under Boolean negation. We introduce a notion of canonical models for MTL, and show that its satisfiability problem is complete for a non-elementary complexity class we call TOWER(poly). We also study the logic FO(∼), the extension of first-order logic with team semantics by unrestricted Boolean negation. We show that its two-variable fragment is decidable, and complete for TOWER(poly) as well. Moreover, we classify the complexity of its model checking problem with respect to the number of variables and the quantifier rank, and prove a dichotomy between PSPACE- and ATIME-ALT(exp, poly)-complete fragments.

Wed 28.11.2018 12-14, C124

Heribert Vollmer: A Complexity Theory for Hard Enumeration Problems (Presentation)

Wed 5.12.2018 12-14, C124

Julian Parsert: Interactive Theorem Proving with Isabelle/HOL

Wed 12.12.2018 12-14, C124

Tuomas Hakoniemi (Barcelona): Size lower bounds for Sums-of-squares proofs

Wed 19.12.2018 12-14, C124

Ulrich Berger (Swansea): On the constructive content of proofs in abstract analysis

Abstract: Can a proof in analysis that does not refer to a particular constructive model of the real numbers have computational content? We show that this is the case by considering an abstract version of Brouwer's Thesis. In its usual formulation Brouwer's Thesis says that every bar is inductive where the notion of a bar involves quantification over infinite sequences of natural numbers. We propose an alternative formulation that avoids infinite sequences and instead uses a coinductive definition to express the bar property. This coinductive formulation behaves better in the context of program extraction from proofs than Brouwer's original formulation. For example, it allows for an equivalent formulation of the Archimedean property as a computationally meaningful induction principle for abstract reals, that is, real numbers only specified by the axioms of a real closed field, but without committing to a particular constructive model. We give two applications, one connected with concurrent computation, the other about the extraction of the fan functional computing a modulus of uniform continuity from a proof that every continuous function on a compact domain is uniformly continuous.