Monadic second-order logic with cardinality predicates

 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: \begin{itemize} \item $\text{}\,\mathrm{Card}(X) = \mathrm{Card}(Y)\,\text{''}$ \item $\text{}\,\mathrm{Card}(X) \text{ belongs to } A\,\text{''}$ \end{itemize} where $A$ is a fixed recursive set of integers.

Let us fix $k$ and a closed formula $F$ in this language.

\begin{conjecture} Is it true that the validity of $F$ for a graph $G$ of tree-width at most $k$ can be tested in polynomial time in the size of $G$? \end{conjecture}

% You may use many features of TeX, such as % arbitrary math (between $...$ and $$...$$) % \begin{theorem}...\end{theorem} environment, also works for question, problem, conjecture, ... % % Our special features: % Links to wikipedia: \Def {mathematics} or \Def[coloring]{Graph_coloring} % General web links: \href [The On-Line Encyclopedia of Integer Sequences]{http://www.research.att.com/~njas/sequences/}

Bibliography

% Example: %*[B] Claude Berge, Farbung von Graphen, deren samtliche bzw. deren ungerade Kreise starr sind, Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10 (1961), 114. % %[CRS] Maria Chudnovsky, Neil Robertson, Paul Seymour, Robin Thomas: \arxiv[The strong perfect graph theorem]{math.CO/0212070}, % Ann. of Math. (2) 164 (2006), no. 1, 51--229. \MRhref{MR2233847} % % (Put an empty line between individual entries)

* indicates original appearance(s) of problem.