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.
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Brown, C. W. Improved projection for cylindrical algebraic decomposition. Journal of Symbolic Computation 32, 5 (Nov. 2001), 447--465. Google ScholarDigital Library
- Chou, S.-C. Mechanical Geometry Theorem Proving. Mathematics and its applications. D. Reidel Publishing Company, Dordrecht, Boston, Lancaster, Tokyo, 1988. Google ScholarDigital Library
- 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 ScholarDigital Library
- Collins, G. E., and Hong, H. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12, 3 (Sept. 1991), 299--328. Google ScholarDigital Library
- Dolzmann, A., and Sturm, T. Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31, 2 (June 1997), 2--9. Google ScholarDigital Library
- Dolzmann, A., and Sturm, T. Simplification of quantifier-free formulae over ordered fields. Journal of Symbolic Computation 24, 2 (Aug. 1997), 209--231. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- Hennig, E., and Halfmann, T. Analog Insydes tutorial. ITWM, Kaiserslautern, Germany, 1998.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarCross Ref
- Lazard, D. Quantifier elimination: Optimal solution for two classical examples. Journal of Symbolic Computation 5, 1&2 (Feb. 1988), 261--266. Google ScholarDigital Library
- 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 ScholarCross Ref
- 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 Scholar
- 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 Scholar
- Strzebonski, A. Solving systems of strict polynomial inequalities. Journal of Symbolic Computation 29, 3 (Mar. 2000), 471--480. Google ScholarDigital Library
- 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 Scholar
- Sturm, T. Reasoning over networks by symbolic methods. Applicable Algebra in Engineering, Communication and Computing 10, 1 (Sept. 1999), 79--96.Google Scholar
- Weispfenning, V. The complexity of linear problems in fields. Journal of Symbolic Computation 5, 1&2 (Feb.--Apr. 1988), 3--27. Google ScholarDigital Library
- 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 ScholarCross Ref
Index Terms
A generic projection operator for partial cylindrical algebraic decomposition
Recommendations
An improvement of the projection operator in cylindrical algebraic decomposition
ISSAC '90: Proceedings of the international symposium on Symbolic and algebraic computationThe Cylindrical Algebraic Decomposition (CAD) method of Collins [5] decomposes r-dimensional Euclidean space into regions over which a given set of polynomials have constant signs. An important component of the CAD method is the projection operation: ...
Constructing a single cell in cylindrical algebraic decomposition
This paper presents an algorithm which, given a point and a set of polynomials, constructs a single cylindrical cell containing the point, such that the given polynomials are sign-invariant in the computed cell. To represent a single cylindrical cell, a ...
Improved Projection for Cylindrical Algebraic Decomposition
McCallum s projection operator for cylindrical algebraic decomposition (CAD) represented a huge step forward for the practical utility of the CAD algorithm. This paper presents a simple theorem showing that the mathematics in McCallum s paper actually ...
Comments