![](/files/happy5.png)
cardinality predicates
Monadic second-order logic with cardinality predicates ★★
Author(s): Courcelle
The problem concerns the extension of Monadic Second Order Logic (over a binary relation representing the edge relation) with the following atomic formulas:
- \item
![$ \text{``}\,\mathrm{Card}(X) = \mathrm{Card}(Y)\,\text{''} $](/files/tex/4e2db7139204fa27f423952041df6049f00cf030.png)
![$ \text{``}\,\mathrm{Card}(X) \text{ belongs to } A\,\text{''} $](/files/tex/3a5b94d5bb93d9aefdfdf917ad8c8535a0328199.png)
where is a fixed recursive set of integers.
Let us fix and a closed formula
in this language.
Conjecture Is it true that the validity of
for a graph
of tree-width at most
can be tested in polynomial time in the size of
?
![$ F $](/files/tex/bfff269cc7df9bdb7c57d8b6a2a74020d114f24d.png)
![$ G $](/files/tex/b8e7ad0330f925492bf468b5c379baec88cf1b3d.png)
![$ k $](/files/tex/c450c3185f7285cfa0b88d3a903c54f7df601201.png)
![$ G $](/files/tex/b8e7ad0330f925492bf468b5c379baec88cf1b3d.png)
Keywords: bounded tree width; cardinality predicates; FMT03-Bedlewo; MSO
![Syndicate content Syndicate content](/misc/feed.png)