en | de

Interactive Theorem Proving

master program

VO2 + PS3  SS 2019  703640 + 703641


Schedule (PS) – Interactive Theorem Proving using Isabelle/HOL

session date topics slides thys solutions
1 06.03 history and motivation, first steps, functional programming in HOL pdf (x1, x4) zip thy
2 13.03 Isabelle basics, higher-order logic, structured proof pdf (x1, x4) zip thy
3 20.03 finding theorems, natural deduction, case analysis, structural induction pdf (x1, x4) zip thy
4 27.03 type definitions, simplification, calculational reasoning pdf (x1, x4) zip thy
5 03.04 PSL - A high-level proof strategy language, Isabelle/ML pdf
6 10.04 sledgehammer, inductive definitions, rule inversion, rule induction pdf (x1, x4) zip thy
7 08.05 code generation, computation induction, multisets pdf (x1, x4) zip thy
8 15.05 session management, document preparation, sets pdf (x1, x4) zip thy
9 22.05 proof methods, well-foundedness, manual termination proofs pdf (x1, x4) zip thy
10 29.05 notation, type classes pdf (x1, x4) zip thy
11 05.06 locales, data type invariants pdf (x1, x4) zip thy
12 12.06 semester projects pdf (x1, x4)
13 19.06 the archieve of formal proofs, the certification approach, IsaFoR/CeTA pdf (x1, x4) zip

Schedule (VO) – Interactive Theorem Proving

session date topics slides sources material
1 07.03 motivation, simple types pdf pdf
2 14.03 pdf pdf
3 21.03 pdf
4 28.03 pdf pdf
5 04.04 pdf
6 11.04 pdf v
7 02.05 pdf v
8 09.05 pdf
9 16.05 pdf pdf
10 23.05 v pdf
11 06.06 pdf v
12 13.06 pdf v
13 27.06 pdf