With the growth in computer power and internet access, an increasing number of problems are solved on remote machines by programs written by experts in a particular field. In this situation, the user may have no knowledge of the algorithm used, its implementation, or indeed how the remote machine is maintained. A mere yes-or-no answer cannot be trusted. We also want a proof of the correctness of the answer. In this talk, we construct such proofs for the problem of graph isomorphism.
Graph isomorphism is vital because every finite combinatorial structure can be encoded in terms of graphs. If two graphs are isomorphic and we are given an isomorphism, then it is easy to prove this by checking the isomorphism. Proving that a pair of graphs are not isomorphic is more difficult. Our proofs are intended to be human-readable, but could be modified to give machine readable proofs using the technologies of Pollet and Sorge.
Graph isomorphism is hard in general. In many cases, invariants give a short and easy-to-verify proof. When no simple invariant can be found to distinguish two graphs, we resort to general graph-isomorphism algorithms. We look at the algorithm of Luks, which takes polynomial time for graphs with bounded vertex degree. We then look at the algorithm of McKay, which is fast in practice but is not known to be polynomial. We have modified both these algorithms to produce human-readable proofs. The modified version of McKay's algorithm can also produce a proof of the correctness of the automorphism group of a graph.
We demonstrate these functions with a demonstration of our Proof Assistant for Graph Nonisomorphism, which is available on the web as a Java applet.