Séminaire du 6 avril 2009. 10h30: *Variant Real Quantifier Elimination: Algorithm, Implementation, Complexity and Application.* Mohab Safey El Din, LIP6 et Projet SALSA de l'Inria Paris-Rocquencourt

We study a *variant* of real quantifier elimination problem
(QE). The variant problem requires the input to satisfy a certain
*extra condition*, and allows the ouput to be *almost*
equivalent to the input. In a sense, we are strengthening the
pre-condition and weakening the post-condition of the standard QE
problem.
The motivation/rationale for studying such a variant QE problem
is that many quantified formulas arising in applications
do satisfy the extra conditions.
Furthermore, in most applications, it is sufficient
that the ouput formula is almost equivalent to the input formula.
We present an algorithm (VQE) , that exploits the strengthened
pre-condition and the weakened post-condition.
The main idea underlying the algorithm is to substitute the repeated
projection step of CAD by a single projection without carrying out a
parametric existential decision over the reals.
We find that the algorithm VQE can tackle important and challenging problems,
such as numerical stability analysis of the widely-used MacCormack's scheme.
The problem has been practically out of reach for standard QE algorithms
in spite of many attempts to tackle it.
However the current implementation of VQE can solve it in about 1
day. Joint work with Hoon Hong, North Carolina State University.

Virginie Collette
Last modified: Mon Mar 30 17:40:36 CEST 2009