Formalizace kombinatoriky na slovech
| advisor: | doc. Ing. Štěpán Starosta, Ph.D. |
| e-mail: | show e-mail |
| type: | bachelor thesis, master thesis |
| branch of study: | MI_MM, MI_AMSM, MINF |
| key words: | formalizace matematiky, kombinatorika na slovech |
| link: | http://users.fit.cvut.cz/~staroste/ |
| description: | 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. |
| references: | [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 |
| last update: | 24.02.2023 12:07:03 |
administrator for this page:
Ľubomíra Dvořáková | last update: 09/12/2011