Formalizace kombinatoriky na slovech

školitel: doc. Ing. Štěpán Starosta, Ph.D.
e-mail: zobrazit e-mail
typ práce: bakalářská práce, diplomová práce
zaměření: MI_MM, MI_AMSM, MINF
klíčová slova: formalizace matematiky, kombinatorika na slovech
odkaz: http://users.fit.cvut.cz/~staroste/
popis: Cílem formalizace matematiky je vyjádřit matematická tvrzení ve formálním jazyku, zapsat v tomto jazyku i jejich důkazy pomocí daných formálních inferenčních pravidel, a jejich správnost algoritmicky ověřit. Práce se týká formalizace matematiky z oblasti kombinatoriky na slovech v generickém dokazovacím asistentu Isabelle/HOL [1]. Práce byla v rámci existujícího projektu formalizace kombinatoriky na slovech [2,3] a výběr konkrétní oblasti by byl po domluvě upřesněn.
literatura: [1] https://isabelle.in.tum.de/
[2] https://gitlab.com/formalcow/combinatorics-on-words-formalized
[3] Š. Holub, Š. Starosta: Formalization of Basic Combinatorics on Words, 12th International Conference on Interactive Theorem Proving (ITP 2021), Liron Cohen and Cezary Kaliszyk (Eds.), Article No. 22; pp. 22:1–22:17, https://doi.org/10.4230/LIPIcs.ITP.2021.22
naposledy změněno: 24.02.2023 12:07:03

za obsah této stránky zodpovídá: Čestmír Burdík | naposledy změněno: 9.9.2021
Trojanova 13, 120 00 Praha 2, tel. +420 770 127 494
České vysoké učení technické v Praze | Fakulta jaderná a fyzikálně inženýrská | Katedra matematiky