Efficient Preprocessing Methods for Quantifier Elimination

  • Christopher W. Brown
  • Christian Gross
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4194)


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.


Hopf Bifurcation Grade Function Prototype Implementation Preprocessing Method Elimination Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Brown, C.W.: Simplification of truth-invariant cylindrical algebraic decompositions. In: Proceedings of the 1998 international symposium on Symbolic and algebraic computation, pp. 295–301. ACM Press, New York (1998)CrossRefGoogle Scholar
  2. 2.
    Brown, C.W.: Simple CAD construction and its applications. Journal of Symbolic Computation 31(5), 521–547 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Brown, C.W.: The QEPCAD B system (2002)Google Scholar
  4. 4.
    Brown, C.W.: The SLFQ system (2002)Google Scholar
  5. 5.
    Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin 37(4), 97–108 (2003)Google Scholar
  6. 6.
    Brown, C.W., El Kahoui, M., Novotni, D., Weber, A.: Algorithmic methods for computing threshold conditions in epidemic modelling. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing (CASC 2004), pp. 51–60. St. Petersburg, Russia (2004)Google Scholar
  7. 7.
    Brown, C.W., McCallum, S.: On using bi-equational constraints in cad construction. In: ISSAC 2005: Proceedings of the 2005 international symposium on Symbolic and algebraic computation, pp. 76–83. ACM Press, New York (2005)CrossRefGoogle Scholar
  8. 8.
    Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition - 20 years of progress. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Heidelberg (1998)Google Scholar
  9. 9.
    Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12(3), 299–328 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Collins, G.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)Google Scholar
  11. 11.
    Dolzmann, A., Sturm, T.: Redlog: Computer algebra meets computer logic. ACM SIGSAM BULLETIN 2-9(31) (1997)Google Scholar
  12. 12.
    Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: ISSAC 2004: Proceedings of the 2004 international symposium on Symbolic and algebraic computation, pp. 111–118. ACM Press, New York (2004)CrossRefGoogle Scholar
  13. 13.
    El Kahoui, M., Weber, A.: Deciding Hopf bifurcations by quantifier elimination in a software-component architecture. Journal of Symbolic Computation 30(2), 161–179 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Loos, R., Weispfenning, V.: Applying linear quantifier elimination. The Computer Journal 5, 450–462 (1993)CrossRefMathSciNetGoogle Scholar
  15. 15.
    McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Dooley, S. (ed.) Proc. International Symposium on Symbolic and Algebraic Computation, pp. 145–149 (1999)Google Scholar
  16. 16.
    McCallum, S.: On propagation of equational constraints in CAD-based quantifier elimination. In: Mourrain, B. (ed.) Proc. International Symposium on Symbolic and Algebraic Computation, pp. 223–230 (2001)Google Scholar
  17. 17.
    van den Driessche, P., Watmough, J.: Reproduction numbers and sub-threshold endemic equilibria for compartmental models of disease transmission. Mathematical Biosciences 180, 29–48 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5(1-2), 3–27 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Xia, Y.: Real solution classifications of parametric semi-algebraic systems. In: Proceedings of A3L (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Christopher W. Brown
    • 1
  • Christian Gross
    • 2
  1. 1.Department of Computer ScienceUnited States Naval AcademyU.S.A.
  2. 2.Institut für Informatik IIUniversität BonnBonnGermany

Personalised recommendations