Courcelle's Theorem Without Logic

2025/05/05 by Yuval Filmus, Filmus, Yuval, Johann A. Makowsky +1
Mathematics · #03C13 #05C85 #68R10 #FOS: Computer and information sciences #History and Theory of Mathematics #Logic in Computer Science (cs.LO) #Mathematics and Applications

paper · pdf · doi:10.48550/arxiv.2505.02771

openalex publication_date 2025/05/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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 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.

Citations

• Meta-theorems for Graph Polynomials
• Twin-width VI: the lens of contraction sequences
• Twin-width I: tractable FO model checking
• Parameterized Algorithms for Modular-Width
• Reflection positivity, rank connectivity, and homomorphism of graphs

Related

• Courcelle's Theorem: A Self-Contained Proof and a Path-Width Variant
• Definability Equals Recognizability for k-Outerplanar Graphs
• Lower Bounds for the Complexity of Monadic Second-Order Logic
• MSOL-Definability Equals Recognizability for Halin Graphs and Bounded Degree k-Outerplanar Graphs
• Definability equals recognizability for graphs of bounded treewidth