Tree-Width for First Order Formulae

We introduce tree-width for first order formulae , fotw(). 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 with fotw() < k into a formula of the k-variable fragment Lk of first order logic. For fixed k, the question whether a given first order formula is equivalent to an Lk 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 con...

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Isolde Adler, Mark Weyer
• Keywords: Automated Reasoning, CSL 2009, Order Formulae, Order Logic, Quantified Constraint Formulae