Isolde Adler ; Mark Weyer - Tree-width for first order formulae

lmcs:786 - Logical Methods in Computer Science, March 29, 2012, Volume 8, Issue 1 -
Tree-width for first order formulaeArticle

Authors: Isolde Adler ; Mark Weyer

    We introduce tree-width for first order formulae \phi, fotw(\phi). We show that computing fotw is fixed-parameter tractable with parameter fotw. Moreover, we show that on classes of formulae of bounded fotw, model checking is fixed parameter tractable, with parameter the length of the formula. This is done by translating a formula \phi\ with fotw(\phi)<k into a formula of the k-variable fragment L^k of first order logic. For fixed k, the question whether a given first order formula is equivalent to an L^k formula is undecidable. In contrast, the classes of first order formulae with bounded fotw are fragments of first order logic for which the equivalence is decidable. Our notion of tree-width generalises tree-width of conjunctive queries to arbitrary formulae of first order logic by taking into account the quantifier interaction in a formula. Moreover, it is more powerful than the notion of elimination-width of quantified constraint formulae, defined by Chen and Dalmau (CSL 2005): for quantified constraint formulae, both bounded elimination-width and bounded fotw allow for model checking in polynomial time. We prove that fotw of a quantified constraint formula \phi\ is bounded by the elimination-width of \phi, and we exhibit a class of quantified constraint formulae with bounded fotw, that has 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, we show that fotw has a characterization in terms of a cops and robbers game without monotonicity cost.

    Volume: Volume 8, Issue 1
    Published on: March 29, 2012
    Imported on: March 2, 2010
    Keywords: Computer Science - Logic in Computer Science,F.2,F.4.1,H.2.3

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1140 times.
    This article's PDF has been downloaded 614 times.