
Courcelle, Bruno
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


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
?




Keywords: bounded tree width; cardinality predicates; FMT03-Bedlewo; MSO
