skip to main content
10.1145/860854.860903acmconferencesArticle/Chapter ViewAbstractPublication PagesissacConference Proceedingsconference-collections
Article

A generic projection operator for partial cylindrical algebraic decomposition

Published:03 August 2003Publication History

ABSTRACT

This paper provides a starting point for generic quantifier elimination by partial cylindrical algebraic decomposition pcad. On input of a first-order formula over the reals generic pcad outputs a theory and a quantifier-free formula. The theory is a set of negated equations in the free variables of the input formula. The quantifier-free formula is equivalent to the input for all parameter values satisfying the theory. For obtaining this generic elimination procedure, we derive a generic projection operator from the standard Collins--Hong projection operator. Our operator particularly addresses formulas with many parameters thus filling a gap in the applicability of pcad. It restricts decomposition to a reasonable subset of the entire space. The above-mentioned theory describes this subset. The approach is compatible with other improvements in the framework of pcad. It turns out that the theory contains assumptions that are easily interpretable and that are most often non-degeneracy conditions. The applicability of our generic elimination procedure significantly extends that of the corresponding regular procedure. Our procedure is implemented in the computer logic system redlog.

References

  1. Arnon, D. S., Collins, G. E., and McCallum, S. Cylindrical algebraic decomposition I: The basic algorithm. SIAM Journal on Computing 13, 4 (Nov. 1984), 865--877. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. Brown, C. W. Guaranteed solution formula construction. In Proceedings of the ISSAC 99, S. Dooley, Ed. ACM Press, New York, NY, July 1999, pp. 137--144. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Brown, C. W. Improved projection for cylindrical algebraic decomposition. Journal of Symbolic Computation 32, 5 (Nov. 2001), 447--465. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Chou, S.-C. Mechanical Geometry Theorem Proving. Mathematics and its applications. D. Reidel Publishing Company, Dordrecht, Boston, Lancaster, Tokyo, 1988. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. Collins, G. E. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Automata Theory and Formal Languages. 2nd GI Conference, H. Brakhage, Ed., vol. 33 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Heidelberg, New York, 1975, pp. 134--183. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Collins, G. E., and Hong, H. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12, 3 (Sept. 1991), 299--328. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Dolzmann, A., and Sturm, T. Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31, 2 (June 1997), 2--9. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Dolzmann, A., and Sturm, T. Simplification of quantifier-free formulae over ordered fields. Journal of Symbolic Computation 24, 2 (Aug. 1997), 209--231. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Dolzmann, A., Sturm, T., and Weispfenning, V. A new approach for automatic theorem proving in real geometry. Journal of Automated Reasoning 21, 3 (1998), 357--380. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. Hennig, E. Rechnergestützte Dimensionierung analoger Schaltungen auf der Basis symbolischer Analyseverfahren. Tech. rep., Zentrum für Mikroelektronik, Universität Kaiserslautern, Dec. 1995. Annual report on a research project.Google ScholarGoogle Scholar
  11. Hennig, E., and Halfmann, T. Analog Insydes tutorial. ITWM, Kaiserslautern, Germany, 1998.Google ScholarGoogle Scholar
  12. Hong, H. An improvement of the projection operator in cylindrical algebraic decomposition. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC 90), S. Watanabe and M. Nagata, Eds. ACM Press, New York, Aug. 1990, pp. 261--264. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Hong, H. Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC 92), P. S. Wang, Ed. ACM Press, New York, July 1992, pp. 177--188. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Hong, H. Quantifier elimination for formulas constrained by quadratic equations via slope resultants. THE Computer Journal 36, 5 (1993), 440--449. Special issue on computational quantifier elimination.Google ScholarGoogle ScholarCross RefCross Ref
  15. Lazard, D. Quantifier elimination: Optimal solution for two classical examples. Journal of Symbolic Computation 5, 1&2 (Feb. 1988), 261--266. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. McCallum, S. Solving polynomial strict inequalities using cylindrical algebraic decomposition. THE Computer Journal 36, 5 (1993), 432--438. Special issue on computational quantifier elimination.Google ScholarGoogle ScholarCross RefCross Ref
  17. McCallum, S. An improved projection operation for cylindrical algebraic decomposition. In Quantifier Elimination and Cylindrical Algebraic Decomposition, B. F. Caviness and J. R. Johnson, Eds. Springer-Verlag, Wien, 1998, pp. 242--268.Google ScholarGoogle Scholar
  18. Seidl, A. An efficient representation of algebraic numbers and polynomials for cylindrical algebraic decomposition (extendend abstract). In Proceedings of the 8th Rhine Workshop on Computer Algebra (Mannheim, Germany, 2002), pp. 167--172.Google ScholarGoogle Scholar
  19. Strzebonski, A. Solving systems of strict polynomial inequalities. Journal of Symbolic Computation 29, 3 (Mar. 2000), 471--480. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Sturm, T. Real Quantifier Elimination in Geometry. Doctoral dissertation, Department of Mathematics and Computer Science. University of Passau, Germany, D-94030 Passau, Germany, Dec. 1999.Google ScholarGoogle Scholar
  21. Sturm, T. Reasoning over networks by symbolic methods. Applicable Algebra in Engineering, Communication and Computing 10, 1 (Sept. 1999), 79--96.Google ScholarGoogle Scholar
  22. Weispfenning, V. The complexity of linear problems in fields. Journal of Symbolic Computation 5, 1&2 (Feb.--Apr. 1988), 3--27. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Weispfenning, V. Quantifier elimination for real algebra---the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing 8, 2 (Feb. 1997), 85--101.Google ScholarGoogle ScholarCross RefCross Ref

Index Terms

  1. A generic projection operator for partial cylindrical algebraic decomposition

    Recommendations

    Comments

    Login options

    Check if you have access through your login credentials or your institution to get full access on this article.

    Sign in
    • Published in

      cover image ACM Conferences
      ISSAC '03: Proceedings of the 2003 international symposium on Symbolic and algebraic computation
      August 2003
      284 pages
      ISBN:1581136412
      DOI:10.1145/860854
      • General Chair:
      • Hoon Hong

      Copyright © 2003 ACM

      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      • Published: 3 August 2003

      Permissions

      Request permissions about this article.

      Request Permissions

      Check for updates

      Qualifiers

      • Article

      Acceptance Rates

      ISSAC '03 Paper Acceptance Rate36of68submissions,53%Overall Acceptance Rate395of838submissions,47%

    PDF Format

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader