Preverjanje kromatičnega števila grafov z dokazovalnim pomočnikom Lean : delo diplomskega seminarja

Kikelj, Gregor (avtor), Bauer, Andrej (mentor), Berčič, Katja (komentor)

V dokazovalniku in programskem jeziku Lean 4 formaliziramo osnove teorije grafov, barvanj in kromatičnega števila. Implementiramo tudi dokazano pravilen algoritem za računanje kromatičnega števila ter analiziramo čas izvajanja. Na koncu implementiramo in dokažemo pravilnost algoritma za preverjanje 2-obarvljivosti v polinomskem času.

• Jezik: Slovenski jezik
• Ključne besede: Lean, Lean 4, graf, kromatično število
• Vrsta gradiva: Delo diplomskega seminarja/zaključno seminarsko delo/naloga
• Tipologija: 2.11 - Diplomsko delo
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2024
• PID: 20.500.12556/RUL-163092
• UDK: 004
• COBISS.SI-ID: 209899011
• Datum objave v RUL: 02.10.2024

Sekundarni jezik

• Jezik: Angleški jezik
• Naslov: Verification of the chromatic number of a graph with the Lean proof assistant

Izvleček

In the Lean 4 proof assistant and programming language, we formalize the basics of graph theory, colorings, and chromatic numbers. We also implement a proven correct algorithm for computing the chromatic number and analyze its running time. Finally, we implement and prove the correctness of an algorithm for checking 2-colorability in polynomial time.

• Ključne besede: Lean, Lean 4, graph, chromatic number