Courcelle's Theorem Without Logic

TL;DR

The paper removes the reliance on Monadic Second Order definability in Courcelle's theorem by replacing it with a purely combinatorial finite-rank condition on a combined matrix built from inductive graph definitions. By leveraging Feferman-Vaught-type composition, Hankel/connection matrices, and a parse-tree framework, it proves that membership of a structure in a property can be decided in time linear in the parse-tree size $m(G)$ whenever the associated combined matrix has finite rank. This generalizes Lovász's approach and extends applicability beyond CMSOL-definable properties to a broad class of properties with finite-rank Hankel/circuit matrices, across width notions such as tree-width, clique-width, and modular-width. The work clarifies the role of logic versus combinatorics in these meta-theorems, provides a versatile framework for new width parameters, and highlights both conceptual gains and challenges, notably in assessing the rank in practice and extending to newer width notions like twin-width.

Abstract

Courcelle's Theorem states that on graphs $G$ of tree-width at most $k$ with a given tree-decomposition of size $t(G)$, graph properties $\mathcal{P}$ definable in Monadic Second Order Logic can be checked in linear time in the size of $t(G)$. Inspired by L. Lovász' work using connection matrices instead of logic, we give a generalized version of Courcelle's theorem which replaces the definability hypothesis by a purely combinatorial hypothesis using a generalization of connection matrices.

Theorems & Definitions (23)

• Theorem 1: Courcelle
• Theorem 2: Courcelle, Makowsky, Rotics
• Theorem 3: Courcelle, Makowsky
• Theorem 4
• Theorem 5: Lovász
• Proposition 6
• Theorem 7
• Theorem 9
• proof
• Definition 10