First-Order Model Checking Problems Parameterized by the Model

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

• Type: Journal
• Year: 2008
• Where: CIE
• Authors: Barnaby Martin
• Keywords: Applied Computing, CIE 2008, Constraint Satisfaction Problem, First-order Logic, Partial Complexity Classification