[madPL] Katherine Cordwell Talk 9/23 1pm-2pm

[LAUREN MARIE NEUDORF <lneudorf@xxxxxxxx>]

Hello!

We are having a guest visitor from CMU, Katherine Cordwell, coming to give a talk on "Formalizing Algorithms for Real Quantifier Elimination", next week on Friday 9/23 at 1pm-2pm in room 4310. 

If you are interested in meeting her for lunch/discussion, sign up using this link (put your name & email underneath the time(s) you are free to meet with her, so I can coordinate between parties): 

https://docs.google.com/spreadsheets/d/11qK4oshoJiyzD3uSVxPe6v7GWhpcVfYW3FstFvRmLjg/edit?usp=sharing

Her abstract is below: 

"Real arithmetic questions involving the âthere existsâ and âfor allâ quantifiers arise in various fields, including formalized mathematics, rigorous engineering domains, and life sciences. Although Tarski proved that real quantified statements can always be reduced to logically equivalent quantifier-free statements through quantifier elimination (QE), QE algorithms are notoriously complicated. This makes QE algorithms difficult to formally verify---formally verified algorithms require accompanying proofs of correctness (typically developed in theorem provers) that rely only on a set of trusted logical axioms---and so in practice, QE problems must be solved with unverified software. This is undesirable given the subtlety of QE algorithms and the safety-critical nature of their applications. In recent work, my collaborators and I found that some of the existing unverified QE tools are self-contradictory on (in total) 137 benchmarks, which underscores the need for more support for practical formally verified QE.

 

My proposed approach is twofold: First, verify a general-purpose multivariate quantifier elimination algorithm based on the Ben-Or, Kozen, and Reif (BKR) algorithm and its variant by Renegar---to fit in a potential âsweet spotâ in between practicality of use and ease of verification. Second, augment BKR with strong additional methods and preprocessing methods, including virtual substitution (an extremely practical QE method for QE problems that involve low-degree polynomials). This talk discusses progress towards this ambitious goal, which includes verifying, in the theorem prover Isabelle/HOL, linear and quadratic virtual substitution, univariate BKR, and a naive multivariate quantifier elimination algorithm that can serve as a stepping-stone to multivariate BKR (in joint work).â"

If you have any questions let me know, 

Lauren