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.