Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Formalizing Macintyre's Theorem in Isabelle-HOL

Fields Institute via YouTube

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
Explore a detailed presentation on formalizing Macintyre's Quantifier Elimination theorem for p-adic numbers using the Isabelle/HOL proof assistant. Delve into the challenges and strategies involved in creating a formally verified proof, including the necessary foundational lemmas and definitions within the Isabelle framework. Learn about the structure of formal proofs, the use of existing proof libraries, and the specific techniques required to adapt mathematical concepts to the constraints of the Isabelle language. Gain insights into topics such as abstract algebra in Isabelle/HOL, locale examples, Denef's proof of Macintyre's theorem, cell decomposition theorems, semialgebraic functions, and boolean algebras of cells. Discover the intricacies of formalizing complex mathematical theorems and the potential for further developments in this field.

Syllabus

Intro
Outline
Introduction to Isabelle/HOL
The Archive of Formal Proofs
Theories in Isabelle
Proofs in Isabelle
Types in Isabelle
Abstract Algebra in Isabelle /HOL: Record Types
Locale Examples
Denef's Proof of Macintyre's Theorem
Cell Decomposition Theorems
Formalizing Denef's Proof: First Steps
Semialgebraic Functions
Semialgebraic Inverses
Multivariable Polynomials
Boolean Algebras of Cells
Further Directions

Taught by

Fields Institute

Reviews

Start your review of Formalizing Macintyre's Theorem in Isabelle-HOL

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.