Szymon Toruńczyk: Model checking first-order logic on graphs of bounded expansion

We give a proof of the result of Dvořák, Kráľ, Thomas which states that for every fixed first-order sentence and class of graphs of bounded expansion there is an algorithm deciding whether the sentence holds in a given graph from the class in linear time. We also discuss some extensions of this result, such as to enumeration problems and to counting problems.