The event will feature three tutorials by:
+ Vasco Brattka (Universität der Bundeswehr München)
Title: Weihrauch Complexity
Abstract: Weihrauch complexity is now an established and active part of mathematical logic. It can be seen as a computability-theoretic approach to classifying the uniform computational content of mathematical problems. This theory has become an important interface between more proof-theoretic and more computability-theoretic studies in the realm of reverse mathematics. In this tutorial we plan to present an introduction into Weihrauch complexity and several facets of this theory. We hope to address most of the following topics:
- An intuitive introduction into Weihrauch complexity with examples.
- The way the Weihrauch lattice can be seen as a general calculus
for mathematical problems. - The role of choice principles within this theory.
- The relation of these principles to axiom systems in reverse
mathematics, as well as to computational classes such as
computability with finitely many mind changes, limit computability, Las Vegas computability etc. - The algebraic structure of the Weihrauch lattice.
- Its relation to linear and intuitionistic logic.
- The way Weihrauch complexity refines Borel complexity.
- Concrete examples of classifications, such as Ramsey’s
theorem, Brouwer’s fixed point theorem etc. - The way certain structural properties of the lattice might
depend on the underlying axiomatic setting (ZFC versus ZF+AD).
The following handbook chapter covers most of the presented topics:
+ Mikoláš Janota (Czech Technical University in Prague)
Title: (Boolean) Satisfiability and its Applications
Abstract: SAT solvers are computer programs that automatically try to decide whether a given Boolean formula is satisfiable or not. Despite the problem being NP-complete, modern SAT solvers are able to solve problems with millions of variables. This enables us to use them to tackle interesting combinatorial problems.
In this tutorial we will look at:
- How problems from other domains can be modeled as Boolean satisfiability.
- Which techniques make SAT solvers so powerful.
- How can SAT be used to solve more expressive logics, pertaining to the domain of satisfiability modulo theories (SMT).
+ Egbert Rijke (University of Ljubljana)
Title: Univalent Combinatorics
Abstract: I will give an introduction to univalent mathematics, and illustrate it with applications of the univalence axiom in combinatorics. Unlike Zermelo-Fraenkel set theory, univalent mathematics is an extension of Martin-Lof’s dependent type theory with the univalence axiom and propositional truncations, and often further extensions are considered as well. The univalence axiom asserts that identifications of types are equivalently described as equivalences of types. A feature of univalent mathematics is that all constructions in it are automatically equivalence invariant. Furthermore, when you define a concept in univalent type theory, you automatically define the type of all objects in that concept. In other words, by defining the concept of group, we get the type of all groups; by defining the concept of n-gon we get the type of all n-gons; by defining the concept of cube, we get the type of all cubes, and so on. In each of these cases, the univalence axiom ensures that the identity type of the type of all objects of a given concept are the isomorphisms or symmetries of that object. We will see that this leads to a natural way of doing group theory via pointed connected 1-types. Furthermore, we will see how the univalence axiom along with some basic homotopy theory helps with the general problem of counting up to isomorphism.