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.