Finite and Algorithmic Model Theory

Motivation

The methods and tools of finite and algorithmic model theory (FAMT) have played an active role in the development of several areas of computer science. Besides the fact that finite or finitely representable structures are those that serve as inputs to computation, the study of the expressive power of logical languages on such structures has led to several fundamental insights. Some of these have found applications in areas as diverse as database theory, computational complexity, random structures and combinatorics, systems verification, automata theory, proof complexity, or algorithmic game theory.

Over the past four decades FAMT has established itself as a solid research field with a strong and evolving community of researchers with a shared research agenda. Much of the progress can be traced to the regular meetings of the community: the last such meeting was at Dagstuhl in 2017, and before that at Les Houches in 2012.

One of the main goals of this Dagstuhl Seminar is to capitalize on the progress and the potential impact of some of the latest developments in FAMT and related areas. Such developments include:

a) The recently established connections between symmetric models of classical computation and bounded-variable counting logics. The symmetric counterparts of classical models of computations include threshold circuits, linear and semidefinite programs, and algebraic circuits. These new results have already been used to establish new upper and lower bounds for large families of algorithms by FAMT tools.

b) The theories of homomorphism counts and limit structures in combinatorics. A recent trend of work establishes that distinguishing the structures by the number homomorphisms they admit from certain classes of patterns, or to certain classes of patterns, is a fruitful alternative to distinguishing them by the logic formulas they satisfy.

c) Enumeration and counting methods including their use in database query processing, among others. One of the goals of this line of research is to understand and classify the logical queries for which it is possible to compute a compact representation of the output from which the query results can be obtained, efficiently, and on demand.

The principal goals of the seminar are the following.

• To identify fresh research challenges in the area of finite and algorithmic model theory, arising from the main application areas, including newly emerging ones.
• To make new connections between core research in FAMT and other subfields of theoretical computer science, such as the theory of combinatorial and continuous optimization algorithms, and the theory of homomorphism counts and limit structures.
• To transfer knowledge from emerging techniques in core FAMT back to the connecting subfields and application areas.
• To strengthen the research community in FAMT, especially by integrating younger members into it.
• To provide continuity to what has been a very successful model for building and consolidating a productive research community in FAMT.