Complexity of Two-Variable First-Order Logics

In this course we explore recent work in the quest for expressive fragments of first-order logics with good algorithmic properties, special attention giving to the two-variable fragment and its intersection with the guarded fragment. While tracing the boundary between decidable and undecidable fragments we describe their power, limitations, similarities and differences in order to stress out key properties responsible for their good or bad behaviour. We also highlight tools and techniques that have proven most effective for designing optimal algorithms for solving the satisfiability or the finite satifiability problems.