During the PHD the goal is to automatically generate and check discharging proofs, in particular for graph coloring. This method is very important in graph theory and had led to important breakthrough such as the 4-color theorem.