Completed
Proofs in Isabelle
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Formalizing Macintyre's Theorem in Isabelle-HOL
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Outline
- 3 Introduction to Isabelle/HOL
- 4 The Archive of Formal Proofs
- 5 Theories in Isabelle
- 6 Proofs in Isabelle
- 7 Types in Isabelle
- 8 Abstract Algebra in Isabelle /HOL: Record Types
- 9 Locale Examples
- 10 Denef's Proof of Macintyre's Theorem
- 11 Cell Decomposition Theorems
- 12 Formalizing Denef's Proof: First Steps
- 13 Semialgebraic Functions
- 14 Semialgebraic Inverses
- 15 Multivariable Polynomials
- 16 Boolean Algebras of Cells
- 17 Further Directions
