Formalizační seminář - NMAG585

• Anglický název: Formalization seminar
• Zajišťuje: Katedra algebry (32-KA)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2023
• Semestr: zimní
• E-Kredity: 2
• Rozsah, examinace: zimní s.:0/2, Z [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Způsob výuky: prezenční
• Další informace: http://www.karlin.mff.cuni.cz/~holub/formalizace.htm
• Poznámka: předmět lze zapsat opakovaně
• Garant: doc. Mgr. Štěpán Holub, Ph.D.

Anotace

čeština

Poslední úprava: 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.

angličtina

Poslední úprava: 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.

Podmínky zakončení předmětu

čeština

Poslední úprava: 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.

angličtina

Poslední úprava: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)

Active participation and formalization of a selected material is required.

Literatura

Poslední úprava: doc. Mgr. Štěpán Holub, Ph.D. (25.08.2023)

Isabelle proof assistant. https://isabelle.in.tum.de/

Archive of formal proofs. https://www.isa-afp.org/