Barvení grafu a formální gramatiky

Abstract

This thesis deals with two equivalent reformulations of the four color problem. The first of them shows the connection between graph coloring and the vector cross product; the se- cond one expands on it and develops a relation to a formal grammar. These reformulations together with the proofs of their equivalence to the four color theorem are the results of two articles motivated by the effort to find a simpler proof of the famous problem, which was proved only by computer. They bring an interesting perspective on the problem of graph coloring and give the possibility to look on it in a new way, which could turn out to be more approachable. This thesis presents the proofs introduced in the source li- terature and adds the steps that are not elaborated in detail by the authors. It aims to formalize some of the ideas and to contribute to the comprehensibility of the proofs. 1

Tato práce se zabývá dvěma ekvivalentními reformulacemi problému čtyř barev. První z nich ukazuje spojitost barvení grafů s vektorovým součinem, druhá na ni navazuje a rozvíjí souvislost s formální gramatikou. Tyto reformulace a důkazy jejich ekvivalence s větou o čtyřech barvách jsou výsledky dvou prací, jejichž motivací je snaha o jednodušší důkaz slavného problému, který byl zatím dokázán jen za pomoci počítače. Přinášejí zajímavý úhel pohledu na problém barvení grafů a nabízejí možnost, jak jej uchopit novým způsobem, který by se mohl ukázat přístupnějším. Tato práce představí důkazy uvedené ve výchozí literatuře a doplní kroky, které tam nejsou podrobně zpracovány. Některé myšlenky se pokusí více formalizovat a přispět tak k lepší srozumitelnosti důkazů. 1