Logical Approaches to Computational Barriers

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 |