Position: PhD candidate
Current Institution: Carnegie Mellon University
Abstract: Towards Practical Provably Correct Algorithms for Real Quantifier Elimination
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: verify the Ben-Or Kozen and Reif (BKR) decision procedure which fits in a potential “sweet spot” in between practicality and ease of verification and augment BKR with strong auxiliary methods and preprocessing methods including virtual substitution (an extremely practical QE method for QE problems that involve low-degree polynomials). My progress towards this goal includes verifying univariate BKR and linear and quadratic virtual substitution (joint work).”
Bio:
Katherine Cordwell is a fifth year Ph.D. student in the Computer Science Department of Carnegie Mellon University (CMU). Her advisor is Andre Platzer. She enjoys research problems in the intersection of computer science and mathematics and is currently interested in formalizing algorithms to perform real quantifier elimination in theorem provers. Her research is partly supported by an NSF GRFP fellowship. Outside of research Katherine has been involved with various outreach programs at CMU most notably TechNights (a program aimed at interesting middle school girls in STEM). Before coming to CMU she graduated with a B.S. in mathematics and a B.S. in computer science from the University of Maryland College Park in 2017.