Assia Mahboubi (LIX)

Constructive quantifier elimination for real numbers and complex

numbers, in a proof assistant [Joint work with Cyril Cohen]

Résumé: The decidability of the first order theories of (discrete) algebraically closed fields and (discrete) real closed fields are well-known results after Tarski's pioneering work in the 40's. Formalizing these proofs in a proof assistant like the Coq system legitimates classical reasoning inside models of these logical fragments, and can also provide complete proof-producing decision procedures for non-linear arithmetic. In this talk we explain how to develop modular formal proofs of quantifier elimination by separating the operations on formulas from the projection theorem at the core of these kind of proofs. The algorithm producing the quantifier free formula is programmed in continuation passing style, which leads to both a concise program and an elegant proof of semantic correctness.