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