id: 05298386
dt: a
an: 05298386
au: Brown, Christopher W.; Gross, Christian
ti: Efficient preprocessing methods for quantifier elimination.
so: Ganzha, Victor G. (ed.) et al., Computer algebra in scientific computing.
    9th international workshop, CASC 2006, Chişinău, Moldova, September
    11‒15, 2006. Proceedings. Berlin: Springer (ISBN
    978-3-540-45182-2/pbk). Lecture Notes in Computer Science 4194, 89-100
    (2006).
py: 2006
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: 
li: doi:10.1007/11870814_7
ab: Summary: This paper presents a framework and prototype implementation for
    preprocessing quantified input formulas that are intended as input for
    quantifier elimination algorithms. The framework loosely follows the AI
    search paradigm ‒ exploring the space of formulas derived from the
    input by applying various rewriting operators in search of a problem
    formulation that will be good input for the intended Q.E. program. The
    only operator provided by the prototype implementation presented here
    is substitution for variables constrained by equations in which they
    appear linearly, supported by factorization and a simple check for
    non-vanishing of denominators in substitutions. Yet we present examples
    of quantified formulas which can be reduced by our preprocessing method
    to problems solvable by current quantifier elimination packages,
    whereas the original formulas had been inaccessible to those.
rv: