Richard Wilke: Logics with Multiteam Semantics
Richard Wilke’s dissertation is devoted to logics for reasoning about dependence and independence. The mathematical basis of such logics is team semantics, an approach that evaluates formulae not just for a single assignment of values to variables but for a set of such assignments, called a team. This makes such logics very powerful and admits reasoning about second-order objects (such as relations or teams) by means of simple first-order syntax. Wilke made a number of substantial contributions to logics with team semantics, including a syntactic characterisation of the union-closed fragments of such logics, and a detailed analysis of the relationship to separation logic, a widely used system for reasoning about programs that mutate data structures. The core of his research concerns the generalisation of logics for dependence and independence to the more powerful setting of multi-teams. A limitation of team semantics is that, based on sets, it does not take into account multiplicities of assignments, and thus provides a purely logical understanding of dependency notions, where only the presence or absence of data is relevant. This is insufficient in scenarios where multiplicities matter, in particular for reasoning about probabilities and statistical independencies. Wilke studied atomic dependency properties of finite multi-teams (i.e., multi-sets of assignments) and defined an appropriate meaning of logical operators for multi-team semantics. He has analysed and compared the properties and expressive power of a number of different logics with team and multi-team semantics and shown that in some important aspects, the latter is quite different from team semantics. For instance, in multi-team semantics, independence is not definable by any combination of properties that are downwards closed or union closed and thus strictly more powerful than inclusion-exclusion logic. He has also studied multi-teams with weights in the real numbers, which leads to notions of topologically open and closed formulae, that he uses to separate variants of multiteam logics with respect to expressive power.