The question whether two graphs are isomorphic is a natural problem which appears in many areas of mathematics and computer science. Since the isomorphisms between two graphs can be described by solutions of a system of equations, algebraic and semi-algebraic proof systems can be used to certify that two graphs are non-isomorphic. In this talk I will discuss the power of the Sherali-Adams, Sums-of-Squares and Polynomial Calculus proof systems for the graph isomorphism problem. I will present results concerning the relative strength of those proof systems via an excursion into the descriptive complexity of the ellipsoid method, and bounded-variable infinitary logics.
This is joint work with Albert Atserias.