Fixed-Point Definability and Polynomial Time on Graphs with Excluded Minors

We prove that fixed-point logic with counting captures polynomial time on all classes of graphs with excluded minors. That is, for every class C of graphs such that some graph H is not a minor of any graph in C, a property P of graphs in C is decidable in polynomial time if and only if it is definable in fixed-point logic with counting. Furthermore, we prove that for every class C of graphs with excluded minors there is a k such that the k-dimensional Weisfeiler-Leman algorithm decides isomorphism of graphs in C in polynomial time. The Weisfeiler-Leman algorithm is a combinatorial algorithm for testing isomorphism. It generalises the basic colour refinement algorithm and is much simpler than the known group-theoretic algorithms for deciding isomorphism of graphs with excluded minors. The main technical theorem behind these two results is a "definables tructure theorem" for classes of graphs with excluded minors. It states that graphs with excluded minors can be decomposed into pieces arranged in a treelike structure, together with a linear order of each of the pieces. Furthermore, the decomposition and the linear orders on the pieces are definable in fixed-point logic (without counting).