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: \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}

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

Fixed-point logic with counting ★★

Author(s): Blass

\begin{question} Can either of the following be expressed in fixed-point logic plus counting: \begin{enumerate} \item Given a graph, does it have a perfect matching, i.e., a set $M$ of edges such that every vertex is incident to exactly one edge from $M$? \item Given a square matrix over a finite field (regarded as a structure in the natural way, as described in [BGS02]), what is its determinant? \end{enumerate} \end{question}

Keywords: Capturing PTime; counting quantifiers; Fixed-point logic; FMT03-Bedlewo

Syndicate content