On the complexity of the model checking problem for syntactic fragments of first-order logic

VCLA hosts a talk by Florent Madelaine

ABSTRACT

Constraint Satisfaction problems (CSPs) have been studied under various names and guise in several communities (variant of SAT, graph colouring, Homomorphism problems, containment of conjunctive queries). Nearly 20 years ago, Feder and Vardi conjectured that every CSP is either in Ptime or NP-complete.

The CSPs can be also seen as a model checking problems for primitive positive sentences (sentences of First-order logic that can be written using only existential predicates and the conjunction). This definition is quite useful as it allows to extend CSPs to the so called Quantified CSPs (QCSPs) by considering model checking problems for positive Horn sentences (as above but with universal quantifiers). QCSPs are Pspace-complete in general and several results suggest a trichotomy between P, NP-complete and Pspace-complete.

We investigate systematically the complexity of the model checking problem for syntactic fragments of first-order logic. We classify all fragments except for CSPs and QCSPs. Most fragments can be classified easily with the exception of positive equality free first-order logic which exhibits some interesting behaviour. 

In this talk we will give an overview of this work and hint at the techniques we used to obtain complexity classifications. Typically these techniques come in three flavours: algebraic (Galois Connection), combinatorial (generalised cores) and logical (quantifier relativisation). 

With kind support by VCLA and WPI.

CONTACT

Stefan Szeider