Preverjanje ravninskosti grafov v Lean : delo diplomskega seminarja

Golob, Gašper (author), Bauer, Andrej (mentor), Berčič, Katja (comentor)

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.

• Language: Slovenian
• Keywords: Dokazovalnik, Lean, ravninski grafi, kombinatorična preslikava
• Work type: Final seminar paper
• Typology: 2.11 - Undergraduate Thesis
• Organization: FMF - Faculty of Mathematics and Physics
• Year: 2022
• PID: 20.500.12556/RUL-140309
• UDC: 510.6
• COBISS.SI-ID: 121263875
• Publication date in RUL: 14.09.2022

Secondary language

• Language: English
• Title: Planarity testing in Lean

Abstract

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.

• Keywords: Proof assistant, Lean, planar graphs, combinatorial map