Courcelle's theorem

In the study of graphalgorithms, Courcelle's theorem is the statement that every graph property definable in the monadic second-orderlogic of graphs can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bruno Courcelle in 1990 and independently rediscovered by Borie, Parker & Tovey (1992). It is considered the archetype of algorithmic meta-theorems.