Tree-Width for First Order Formulae
Tree-Width for First Order Formulae
复制标题
一阶公式的树宽度
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Weyer
中科院分区：
文献类型：
--
作者：
Isolde Adler;M. Weyer
本文对一阶公式φ，fotw（φ）引入树宽。我们表明，计算fotw是固定参数易处理的参数fotw。此外，我们还证明了在有界函数的公式类上，模型检验是固定参数易处理的，参数是公式的长度。这是通过将公式φ（fotw（φ）< k）转换为一阶逻辑的k变量片段Lk的公式来完成的。对于固定的k，给定的一阶公式是否等价于Lk公式的问题是不可判定的。相反，具有有界边界的一阶公式类是等价可判定的一阶逻辑的片段。
我们的概念树宽度一般树宽度的合取查询的任意公式的一阶逻辑考虑到量词的相互作用在一个公式。此外，它比Chen和Dalmau（CSL 2005）定义的量化约束公式的消除宽度的概念更强大：对于量化约束公式，有界消除宽度和有界fotw都允许在多项式时间内进行模型检查。证明了量化约束公式φ的fotw由φ的消去宽度有界，并给出了一类fotw有界的量化约束公式，其消去宽度为无界.对于Flum、弗里克和Grohe（JACM 49，2002）定义的非递归分层数据集的严格树宽，也有类似的比较。
最后，我们证明了fotw是一个没有单调代价的强盗和警察博弈的刻画。
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 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 φ is bounded by the elimination-width of φ, 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 robber and cops game without monotonicity cost.