Who is... Isabelle, and why is she so picky about my proofs?

Vortrag von Dr. Dmitriy Traytel

Datum: 17.04.18  Zeit: 17.15 - 18.30  Raum:

Isabelle is a generic proof assistant. It provides its users with different languages and logical foundations to carry out formal proofs whose individual proof steps are mechanically checked for correctness. In this talk, I will focus on Isabelle/HOL— Isabelle's most widely used and developed logical foundation of higher-order logic. I will survey in a hands-on demonstration of the system the foundations of Isabelle/HOL, its mathematical libraries, and the available specification and proof automation tools that help users to deal with Isabelle's harsh judgments of what constitutes a formal proof.