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.
