Tree-Width for First Order Formulae

DOI10.1007/978-3-642-04027-6_8MaRDI QIDQ3644741zbMATH OpenOpenAlexFDO

Authors Isolde Adler, Mark Weyer

Publication date 12 November 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1203.3814

Mathematics Subject Classification ID

Classical first-order logic (03B10) Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15)

Abstract: 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.

Recommendations

• Tree-width for first order formulae
• Tree-width in algebraic complexity
• First-order aspects of tree paths
• First-order tree-to-tree functions
• The tree-width of C
• Computing tree width: from theory to practice and back
• Width functions for hypertree decompositions
• scientific article; zbMATH DE number 1944139
• scientific article; zbMATH DE number 1859215
• Treewidth computations. I: Upper bounds

Cites work

• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• Computer Science Logic
• Conjunctive query containment revisited
• Conjunctive-query containment and constraint satisfaction
• Digraph Decompositions and Monotonicity in Digraph Searching
• Directed tree-width examples
• Graph searching and a min-max theorem for tree-width
• Hypertree decompositions and tractable queries
• Marshals, monotone marshals, and hypertree-width
• Query evaluation via tree-decompositions
• Robbers, marshals, and guards: Game theoretic and logical characterizations of hypertree width.
• The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory
• Tree-Related Widths of Graphs and Hypergraphs

Cited in

(4)

• Tree-width for first order formulae
• Decomposing quantified conjunctive (or disjunctive) formulas
• Twin-width. I: Tractable FO model checking
• Tree-depth, quantifier elimination, and quantifier rank

This page was built for publication: Tree-Width for First Order Formulae

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3644741)