# Definability equals recognizability for graphs of bounded treewidth

arXiv: https://arxiv.org/abs/1605.03045 · HTML: https://mlsanity.com/paper/1605.03045/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 May 2016.

## Built on by (most cited first, 1 of 1)

- [From Width-Based Model Checking to Width-Based Automated Theorem Proving](https://mlsanity.com/paper/2205.10995/) (2022)

## Abstract (arXiv)

We prove a conjecture of Courcelle, which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the following sense: constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. While the forward implication is a classic fact known as Courcelle's theorem, the converse direction remained open