Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)
Seminar is intended for those interested in interactive proof systems that allow formal verification of mathematical
proofs. The content of the seminar is a hands on introduction to the Isabelle/HOL proof assistant at the user level
allowing the formalization of specific selected topics.
Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)
Určeno pro zájemce o interaktivní důkazové systémy, které umožňují formální verifikaci matematických důkazů.
Obsahem semináře je seznámení s důkazovým asistentem Isabelle/HOL na uživatelské úrovni umožňující
formalizaci konkrétních vybraných témat.
Course completion requirements -
Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)
Active participation and formalization of a selected material is required.
Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)
Zápočet bude udělen za aktivní účast na semináři a za formalizaci vybraného materiálu.
Literature - Czech
Last update: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)