A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
summary
Formal verification of a first complete multivariate QE in Isabelle/HOL that hybridizes Ben-Or‑Kozen‑Reif and Tarski: it reduces quantifier elimination to sign determination, builds matrix equations with reduction, generalizes Tarski queries using pseudo‑remainder sequences, and exports executable SML via Isabelle’s code generator. The development is ~8500 lines on AFP, reuses a virtual‑substitution preprocessor for speed, proves logical correctness end‑to‑end but is currently not competitive on performance and lacks a fully verified code generator.
AI-written summary · about