en | de

Interaktives Beweisen in Isabelle/HOL

Masterstudium

VU3  SS 2022  703315

Slides

The slides will be made avaiable during the semester.

  1. Organization, Introduction, Higher-Order Logic (4 on 1) and Demo01.thy
  2. Pure Framework, Structured Proofs (4 on 1) and Demo02.thy
  3. Structured Proofs Continued, Case Analysis and Induction (4 on 1) and Demo03.thy
  4. Induction Revisited, Calculation Reasoning, Simplifier (4 on 1) and Demo04.thy
  5. Function Definitions Revisited, Manual Termination Proofs, Attributes (4 on 1) and Demo05.thy
  6. Projects, Proof Methods, Sledgehammer (4 on 1) and Demo06.thy
  7. Inductive Definitions, Rule Inversion and Induction (4 on 1) and Demo07.thy
  8. Sets and Lists in Isabelle, Case Study: Binary Search Trees (4 on 1) and Demo08.thy (Demo08_completed.thy)
  9. Typedef, Lifting and Transfer (4 on 1) and Demo09.thy
  10. Code Generation – Part 1 (4 on 1) and Demo10.thy
  11. Code Generation – Part 2 (4 on 1) and Demo11.thy
  12. Sessions, Document Preparation, Type Classes (4 on 1) and Demo12.thy and session12.tgz
  13. Further Topics, Master Projects (4 on 1) and Demo13.thy