Given a graph, we are often interested in deciding if it satisfies a certain property. Some examples of graph properties include connectivity, bipartiteness, and planarity. Courcelle's theorem gives parameterized upper bounds for decidability for a wide class of graph properties. Specifically, Courcelle's theorem is a metatheorem that states that if a graph property is definable in monadic second-order logic on graphs, then the property is decidable in linear fixed-parameter tractable time with the graph treewidth as the parameter. This theorem finds many uses in automata theory and model checking. We will study the theorem and look at some of its applications.
