Variant Quantifier Elimination

Hoon Hong 1 Mohab Safey El Din 2, 3
3 PolSys - Polynomial Systems
LIP6 - Laboratoire d'Informatique de Paris 6, Inria Paris-Rocquencourt
Abstract : We describe an algorithm (VQE)\ for a \emph{variant} of the real quantifier elimination problem (QE). The variant problem requires the input to satisfy a certain \emph{extra condition}, and allows the output to be \emph{almost} equivalent to the input. 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 output formula is almost equivalent to the input formula. 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 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 12 hours. This paper extends the results reported at the conference ISSAC~2009.
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 2012, International Symposium on Symbolic and Algebraic Computation (ISSAC 2009), 47 (7), pp.883-901. <10.1016/j.jsc.2011.05.014>
Liste complète des métadonnées


https://hal.inria.fr/hal-00778365
Contributeur : Mohab Safey El Din <>
Soumis le : samedi 19 janvier 2013 - 19:12:37
Dernière modification le : mardi 30 mai 2017 - 01:12:07
Document(s) archivé(s) le : samedi 20 avril 2013 - 03:54:20

Fichier

vqe_jsc_final.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Hoon Hong, Mohab Safey El Din. Variant Quantifier Elimination. Journal of Symbolic Computation, Elsevier, 2012, International Symposium on Symbolic and Algebraic Computation (ISSAC 2009), 47 (7), pp.883-901. <10.1016/j.jsc.2011.05.014>. <hal-00778365>

Partager

Métriques

Consultations de
la notice

223

Téléchargements du document

161