Anotace
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.
