Transproof : Computer assisted graph transformations

Over the years, several softwares and tools have appeared in order to help in to find conjectures in Extremal Graph Theory. One of these tools is PHOEG which is currently being developed in our team as a sucessor to GraPHedron. The conjectures usually consist in the definition of a class of graphs, called extremal graphs, that realize a bound for some graph invariant given some constraints. These constraints can vary from fixing the value of another invariant to restricting the graphs to a specific class.

An example of a graph invariant is the average eccentricity. Let G = (V,E) be a graph and v in V be a vertex of G, we define the eccentricity of v as the maximal distance between v and any other vertex of G. The average eccentricity as well as the average distance are used in a conjecture (Aouchiche, PhD Thesis, 2006) stating that among all connected graphs on n vertices, the graph that maximizes the difference between the average eccentricity and the average distance is the path on n vertices.

This conjecture is one among many others generated by the existing tools. Indeed, while some of them provide support to filter trivial or false conjectures, they still produce an important number of non trivial ones.

To help researchers in handling this quantity of conjectures, we develop a PHOEG module called Transproof. This module enables its users to study graph transformations. These transformations can then be used in proving the extremality of a class of graphs. This is done by proving that any non extremal graph concerned by the conjecture can be transformed into a new graph whose value for the studied invariant is strictly closer to the conjectured bound. Such a proof technique is called a proof by transformation and is widely used in Extremal Graph Theory.

Transproof uses a graph database to store graph transformations in the form of a metagraph with graphs as its vertices and applications of transformations as its arcs. It uses an exact approach on small graphs and provides the researchers with means to explore graph transformations as well as to test ideas to prove the conjectures.

In this talk, we explain the difficulties encountered when building and exploiting this data and the ideas used to handle them. Using the conjecture explained above, we also illustrate how Transproof can help to raise ideas in the design of a proof by transformation.