Preverjanje ravninskosti grafov v LeanGolob, Gašper (Avtor) Bauer, Andrej (Mentor) Berčič, Katja (Komentor) DokazovalnikLeanravninski grafikombinatorična preslikavaZa 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.20222022-09-14 08:15:24Delo diplomskega seminarja/zaključno seminarsko delo/naloga140309UDK: 510.6VisID: 127031COBISS_ID: 121263875sl