First-order model checking problems parameterized by the model

We study the complexity of the model checking problem, for fixed models <em>A</em>, over certain fragments $\mathcal{L}$ of first-order logic, obtained by restricting which of the quantifiers and boolean connectives we permit. These are sometimes known as the expression complexities of $\mathcal{L}$. We obtain various full and partial complexity classification theorems for these logics $\mathcal{L}$ as each ranges over models <em>A</em>, in the spirit of the dichotomy conjecture for the Constraint Satisfaction Problem --- which itself may be seen as the model checking problem for existential conjunctive positive first-order logic.

Martin B. (2008) First-Order Model Checking Problems Parameterized by the Model. In: Beckmann A., Dimitracopoulos C., Löwe B. (eds) Logic and Theory of Algorithms. CiE 2008. Lecture Notes in Computer Science, vol 5028. Springer, Berlin, Heidelberg