Decomposing First-Order Logic

Hubie Chen from Universitat Pompeu Fabra, Barcelona held a talk on May 7th, 2012

ABSTRACT

Model checking--deciding if a logical sentence holds on a structure--is a basic computational task that is well-known to be intractable in general. For first-order logic on finite structures, it is PSPACE-complete, and the natural evaluation algorithm exhibits exponential dependence on the formula. This general intractability naturally prompts the search for structural properties of formulas that imply tractability, and an understanding of the complexity of model checking on restricted sets of sentences. Conjunctive queries (sentences built from conjunction and existential quantification) have been heavily studied from this viewpoint. One approach to restricting conjunctive queries is to restrict the so-called primal graph of a query (where two variables are linked if they occur together in an atom); a classical result is that model checking is tractable on primal graphs of bounded treewidth, and a matching intractability result was given by Grohe, Schwentick, and Segoufin (2001).

After presenting the background and context for this research direction, we will discuss recent results on two fragments of first-order logic. First, we will look at model checking the quantified conjunctive fragment of first-order logic, that is, prenex sentences built from conjunction, and both universal and existential quantification. Each such sentence naturally induces a prefixed graph, by which is meant the primal graph paired with the quantifier prefix. We present a (recently obtained) comprehensive complexity classification of the sets of prefixed graphs on which model checking is tractable, based on a novel generalization of treewidth, that generalizes and places into a unified framework a number of existing results on quantified formulas.

We will next discuss recent results on existential positive logic (sentences built from conjunction, disjunction, and existential quantification). We present a classification result for the case of bounded arity, which shows that a sentence set is fixed-parameter tractable if and only if each sentence can be expressed in bounded-variable logic. Indeed, expressivity in bounded-variable logic gives, for both fragments, a uniform explanation for fixed-parameter tractability. In the case of existential positive logic, however, one has a divergence between parameterized and classical tractability: there are simple sentence sets that are fixed-parameter tractable but NP-complete. We consider the length needed to translate such sentence sets into bounded-variable logic, proving a superpolynomial lower bound; this gives a new type of formula size lower bound and a way to understand the divergence between fixed-parameter tractability and polynomial-time tractability.

We will conclude with a discussion of open directions and questions.