Formalizing Macintyre's Theorem in Isabelle-HOL

Formalizing Macintyre's Theorem in Isabelle-HOL

Fields Institute via YouTube Direct link

Semialgebraic Functions

13 of 17

13 of 17

Semialgebraic Functions

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. 1 Intro
  2. 2 Outline
  3. 3 Introduction to Isabelle/HOL
  4. 4 The Archive of Formal Proofs
  5. 5 Theories in Isabelle
  6. 6 Proofs in Isabelle
  7. 7 Types in Isabelle
  8. 8 Abstract Algebra in Isabelle /HOL: Record Types
  9. 9 Locale Examples
  10. 10 Denef's Proof of Macintyre's Theorem
  11. 11 Cell Decomposition Theorems
  12. 12 Formalizing Denef's Proof: First Steps
  13. 13 Semialgebraic Functions
  14. 14 Semialgebraic Inverses
  15. 15 Multivariable Polynomials
  16. 16 Boolean Algebras of Cells
  17. 17 Further Directions

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.