Tree-width for first-order formulas

Joint work with Mark Weyer, Humboldt University Berlin

We introduce tree-width for first-order formulas, fotw.  We show that
on classes of formulas of bounded fotw, model checking is fixed
parameter tractable, with parameter the length of the formula. This is
done by translating a formula with fotw < k into a formula of the
k-variable fragment of first-order logic.  For fixed k, the question
whether a given first-order formula is equivalent to a formula of the
k-variable fragment, is undecidable. In contrast, the classes of
first-order formulas with bounded fotw are fragments of first-order
logic for which the equivalence is decidable.  Moreover, computing
fotw is fixed-parameter tractable with parameter fotw.  Our notion of
fotw generalises tree-width of conjunctive queries to arbitrary
formulae of first-order logic by taking into account the quantifier
interaction in a formula. Fotw is more powerful than the notion of
elimination-width of quantified constraint formulae, defined by Chen
and Dalmau (CSL 2005): For quantified constraint formulas, both
bounded elimination-width and bounded fotw allow for model checking in
polynomial time.  The first-order tree-width of a quantified
constraint formula is bounded by its elimination-width, and there are
classes of quantified constraint formulas with bounded fotw, that have
unbounded elimination-width.  A similar comparison holds for strict
tree-width of non-recursive stratified datalog as defined by Flum,
Frick, and Grohe (JACM 49, 2002).  Finally, fotw has a
characterization in terms of a robber and cops game without
monotonicity cost.