Quantifier Elimination for Constraint Logic Programming

  • Thomas Sturm
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3718)


We present an extension of constraint logic programming, where the admissible constraints are arbitrary first-order formulas over various domains: real numbers with ordering, linear constraints over p-adic numbers, complex numbers, linear constraints over the integers with ordering and congruences (parametric Presburger Arithmetic), quantified propositional calculus (parametric qsat), term algebras. Our arithmetic is always exact. For ℝ are ℂ there are no restrictions on the polynomial degree of admissible constraints. Constraint solving is realized by effective quantifier elimination. We have implemented our methods in our system clp(rl). A number of computation examples with clp(rl) are given in order to illustrate the conceptual generalizations provided by our approach and to demonstrate its feasibility.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. In: Matzat, B.H., Greuel, G.M., Hiss, G. (eds.) Algorithmic Algebra and Number Theory, pp. 221–247. Springer, Berlin (1998)Google Scholar
  2. 2.
    Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: Dooley, S. (ed.) Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation (ISSAC 1999), Vancouver, BC, pp. 129–136. ACM Press, New York (1999)CrossRefGoogle Scholar
  3. 3.
    Sturm, T., Weispfenning, V.: Quantifier elimination in term algebras. The case of finite languages. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing. Proceedings of the CASC 2002, pp. 285–300. TUM München (2002)Google Scholar
  4. 4.
    Hong, H.: RISC-CLP(Real): Constraint logic programming over real numbers. In: Benhamou, F., Colmerauer, A. (eds.) Constraint Logic Programming: Selected Research. MIT Press, Cambridge (1993)Google Scholar
  5. 5.
    Colmerauer, A., et al.: Workshop on first-order constraints, Marseille, France. Abstracts of talks (2001)Google Scholar
  6. 6.
    Dolzmann, A., Sturm, T.: Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31, 2–9 (1997)CrossRefGoogle Scholar
  7. 7.
    Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12, 299–328 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5, 3–27 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Weispfenning, V.: Quantifier elimination for real algebra—the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing 8, 85–101 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Becker, E., Wörmann, T.: On the trace formula for quadratic forms. In: Jacob, W.B., Lam, T.Y., Robson, R.O. (eds.) Recent Advances in Real Algebraic Geometry and Quadratic Forms. Contemporary Mathematics, vol. 155, pp. 271–291. American Mathematical Society, Providence (1994); Proceedings of the RAGSQUAD Year, Berkeley, (1990–1991)Google Scholar
  11. 11.
    Pedersen, P., Roy, M.F., Szpirglas, A.: Counting real zeroes in the multivariate case. In: Eysette, F., Galigo, A. (eds.) Computational Algebraic Geometry, Berlin. Progress in Mathematics, vol. 109, pp. 203–224. Birkhäuser, Boston (1993); Proceedings of the MEGA 1992 Google Scholar
  12. 12.
    Weispfenning, V.: A new approach to quantifier elimination for real algebra. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 376–392. Springer, Wien (1998)Google Scholar
  13. 13.
    Sturm, T.: Linear problems in valued fields. Journal of Symbolic Computation 30, 207–219 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Weispfenning, V.: Comprehensive Gröbner bases. Journal of Symbolic Computation 14, 1–29 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Weispfenning, V.: Complexity and uniformity of elimination in Presburger arithmetic. In: Küchlin, W.W. (ed.) Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation (ISSAC 1997), Maui, HI, pp. 48–53. ACM Press, New York (1997)CrossRefGoogle Scholar
  16. 16.
    Seidl, A., Sturm, T.: Boolean quantification in a first-order context. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing. Proceedings of the CASC 2003, pp. 345–356. TUM München (2003)Google Scholar
  17. 17.
    Dincbas, M., Van Hentenryck, P., Simonis, H., Aggoun, A., Graf, T., Berthier, F.: The constraint logic programming language CHIP. In: Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, Japan, Decemeber 1988, pp. 693–702. Ohmsha Publishers, Tokyo (1988)Google Scholar
  18. 18.
    Jaffar, J., Michaylov, S., Stuckey, P.J., Yap, R.H.C.: The CLP(R) language and system. ACM Transactions on Programming Languages and Systems 14, 339–395 (1992)CrossRefGoogle Scholar
  19. 19.
    Colmerauer, A.: Prolog III. Communications of the ACM 33, 70–90 (1990)CrossRefGoogle Scholar
  20. 20.
    Dolzmann, A., Sturm, T.: Simplification of quantifier-free formulae over ordered fields. Journal of Symbolic Computation 24, 209–231 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Frühwirth, T., Abdennadher, S.: Essentials of Constraint Programming. Springer, Heidelberg (2003)Google Scholar
  22. 22.
    Kameny, S.L.: Roots: A reduce root finding package. In: Hearn, A.C., Codemist, Ltd. (eds.) Reduce User’s and Contributed Packages Manual Version 3.7, pp. 513–518. Anthony C. Hearn and Codemist Ltd. (1999)Google Scholar
  23. 23.
    Sturm, T., Weispfenning, V.: Computational geometry problems in Redlog. In: Wang, D. (ed.) ADG 1996. LNCS(LNAI), vol. 1360, pp. 58–86. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Thomas Sturm
    • 1
  1. 1.FMIUniversität PassauPassauGermany

Personalised recommendations