Importance: Medium ✭✭
 Author(s): Courcelle, Bruno
 Subject: Logic » Finite Model Theory
 Keywords: bounded tree width cardinality predicates FMT03-Bedlewo MSO
 Posted by: dberwanger on: May 18th, 2012

The problem concerns the extension of Monadic Second Order Logic (over a binary relation representing the edge relation) with the following atomic formulas:

\item \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 ?

## Bibliography

* indicates original appearance(s) of problem.