Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
First-Order Model Checking Problems Parameterized by the Model

Speaker: Barnaby Martin
Slot: Array, 11:40-12:00, col. 5


We study the complexity of the model checking problem, for fixed models A, over
certain fragments 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 L. We obtain various full and partial complexity
classification theorems for these logics L 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.

websites: Arnold Beckmann 2008-05-18