Tree-width for first order formulae
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/786/pdf |
| _version_ | 1797268738579365888 |
|---|---|
| author | Isolde Adler Mark Weyer |
| author_facet | Isolde Adler Mark Weyer |
| author_sort | Isolde Adler |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:37:15Z |
| format | Article |
| id | doaj.art-fe663bbcca434c59a6a11224a1ce9361 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:15Z |
| publishDate | 2012-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-fe663bbcca434c59a6a11224a1ce93612024-03-08T09:27:55ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-03-01Volume 8, Issue 110.2168/LMCS-8(1:32)2012786Tree-width for first order formulaeIsolde AdlerMark WeyerWe 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.https://lmcs.episciences.org/786/pdfcomputer science - logic in computer sciencef.2f.4.1h.2.3 |
| spellingShingle | Isolde Adler Mark Weyer Tree-width for first order formulae Logical Methods in Computer Science computer science - logic in computer science f.2 f.4.1 h.2.3 |
| title | Tree-width for first order formulae |
| title_full | Tree-width for first order formulae |
| title_fullStr | Tree-width for first order formulae |
| title_full_unstemmed | Tree-width for first order formulae |
| title_short | Tree-width for first order formulae |
| title_sort | tree width for first order formulae |
| topic | computer science - logic in computer science f.2 f.4.1 h.2.3 |
| url | https://lmcs.episciences.org/786/pdf |
| work_keys_str_mv | AT isoldeadler treewidthforfirstorderformulae AT markweyer treewidthforfirstorderformulae |