摘要：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)
其他关键词：treewidth, model checking, conjunctive queries, quantified constraint formulae, first-order logic, elimination-width, cops and robbers game.
