MAT 180 Computer proofs (Matthias Köppe; Winter 2022)

MAT 180 Computer proofs (Matthias Köppe; Winter 2022)
This is a quarter-long upper-division undergraduate course on Computer Proofs, held in Winter 2022. The videos are edited versions of the synchronously held lectures, with lengthy interactions with students edited out or compressed. All notes were written in real time.

The following topics are covered in this course:

  • Proofs, certificates, theorems of the alternative
  • Modeling with propositional logic in z3
  • SAT and NP reductions
  • Quantifier elimination by propositional resolution
  • Quantifier elimination in the theory of linear inequalities over the reals
  • Quantifier elimination in disjunctions of equation/inequality/congruence systems over the integers
  • Helly-type reductions for infeasible inequality systems over the reals and integers
  • Incomputability of polynomial Diophantine systems: Davis-Putnam-Robertson-Matiyasevich theorem 
  • Polynomial systems over the reals: Real nullstellensatz, positivstellensatz, sums of squares
  • Decompositions of proofs
Videos and all other materials are copyright 2022 Matthias Köppe and shared as Open Educational Resources subject to the Creative Commons Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0) license.

…Read more Less…
 Public, Restricted
28 Media
1 Members
Managers:
 Matthias Koeppe
Appears In:
Math & ScienceMathematics