20.500.12556/RUL-140309 Preverjanje ravninskosti grafov v Lean delo diplomskega seminarja Planarity testing in Lean 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. 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. Dokazovalnik Lean ravninski grafi kombinatorična preslikava Proof assistant Lean planar graphs combinatorial map true false false Slovenski jezik Angleški jezik Delo diplomskega seminarja/zaključno seminarsko delo/naloga 2022-09-14 08:15:24 2022-09-14 08:15:25 2024-05-29 12:06:32 0000-00-00 00:00:00 2022 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 127031 121263875 5335.pdf 5335.pdf 1 2FADB84494444FA710052ABD344C75EC d7f54dec2d0b5e08e2f60bc1fca728599b785c7af292b0db25577d70b0f442e5 8e2849cd-33f4-11ed-92af-00155dcfd717 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=161017 5336.zip 5336.zip 1 E32A32A11ABE365386ADA2A139FFD9C5 90a1d4d128e2b6035ed86f40eb4ffdfe599704c80989f1743e68f563bca8e9a2 8e2a5c35-33f4-11ed-92af-00155dcfd717 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=161018 Fakulteta za matematiko in fiziko 0 0 0