Seminar talks fall 2018
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.