Preverjanje ravninskosti grafov v Lean : delo diplomskega seminarja

Golob, Gašper (avtor), Bauer, Andrej (mentor), Berčič, Katja (komentor)

Za namene formalizacije ravninskih grafov v dokazovalniku Lean uvedemo matematični pojem kombinatoričnih preslikav in zanj predstavimo karakterizacijo ravninskih grafov, za katero dokažemo tudi smiselnost. Pojem kombinatoričnih preslikav v dokazovalniku Lean formaliziramo na način, ki omogoča lastnosti, s katerimi lahko neposredno računamo. Formaliziramo dokaz, da so tako podane kombinatorične preslikave skladne z njihovo matematično definicijo.

• Jezik: Slovenski jezik
• Ključne besede: Dokazovalnik, Lean, ravninski grafi, kombinatorična preslikava
• Vrsta gradiva: Diplomsko delo/naloga
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2022
• PID: 20.500.12556/RUL-140309
• UDK: 510.6
• COBISS.SI-ID: 121263875
• Datum objave v RUL: 14.09.2022

Sekundarni jezik

• Jezik: Angleški jezik
• Naslov: Planarity testing in Lean

Izvleček

For the purposes of formalizing planar graphs in the proof assistant Lean, we define combinatorial maps and show how they characterize planar graphs, where we also prove the correctness of the characterization. Using Lean we formalize combinatorial maps in such a way, that their properties can be computed. Finally we show that the given formalization of combinatorial maps corresponds to the mathematical definition of combinatorial maps.

• Ključne besede: Proof assistant, Lean, planar graphs, combinatorial map