First-order model checking problems parameterized by the model

Abstract

We study the complexity of the model checking problem, for fixed models A, over certain fragments 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 . We obtain various full and partial complexity classification theorems for these logics as each ranges over models A, 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. © 2008 Springer-Verlag Berlin Heidelberg.