Abstract:

It is known that model checking of conjunctive queries of bounded tree-width
is in P-time. We show how this can be done and generalize this approach to
full first order logic.

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.

Joint work with Mark Weyer, Humboldt University Berlin

Bio:
Isolde Adler works in
Finite Model Theory and Graph Algorithms. 
She got her PhD in 2006 in Freiburg, Germany. 
Currently she is a Junior Professor
at the Goethe University in Frankfurt. Previously she held positions at the
Humboldt University, Berlin and University of Bergen, Norway.