Hilbertova věta o bázi v Isabelle/HOL
| Název práce v češtině: | Hilbertova věta o bázi v Isabelle/HOL |
|---|---|
| Název v anglickém jazyce: | Hilbert basis theorem in Isabelle/HOL |
| Akademický rok vypsání: | 2023/2024 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | |
| Ústav: | Katedra algebry (32-KA) |
| Vedoucí / školitel: | doc. Mgr. Štěpán Holub, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 06.11.2023 |
| Datum zadání: | 08.11.2023 |
| Datum potvrzení stud. oddělením: | 10.11.2023 |
| Zásady pro vypracování |
| Student prostuduje Hilbertovu větu o bázi v kontextu aplikace na řešitelné grupy. Tuto větu formalizuje v důkazovém assistentu Isabelle/HOL a popíše principy této formalizace. |
| Seznam odborné literatury |
| N. Jacobson, Basic Algebra II, Freeman 1982
P. Hall, Finiteness Conditions for Soluble Groups, Proc. London Math. Soc. (3) 4 (1954) 419–436 T. Nipkow, L. C. Paulson, M. Wenzel, Isabelle/HOL: a proof assistant for higher-order logic, 2023 C. Ballarin, Exploring the Structure of an Algebra Text with Locales, J. Autom. Reasoning 64 (2020) 1093–1121 |