Computational perspectives on the classical decision problema vade mecum

The classical decision problem for first-order logic asks whether a given sentence of first-order logic is satisfiable, i.e. whether it is true in some structure. While this problem is undecidable for first-order logic as a whole, its restrictions to certain fragments of first-order logic are known to admit of an effective solution. One of the central goals of research in mathematical logic in recent decades has been to determine the decidability and complexity of this problem for different fragments of first-order logic.

This course surveys major decidable fragments of first-order logic, including the two-variable, guarded, and fluted fragments, along with their extensions with counting quantifiers. These logics present different challenges, often requiring specialized techniques such as reduction to integer programming, small model constructions, tree decompositions, variable elimination, and reduction to tiling problems. We provide a comprehensive treatment of these techniques and briefly survey some open problems.