Partial cylindrical algebraic decomposition for quantifier elimination.

*(English)*Zbl 0754.68063From the authors’ abstract: “The Cylindrical Algebraic Decomposition method (CAD) decomposes \(R^ n\) into regions over which given polynomials have constant signs. An important application of CAD is quantifier elimination in elementary algebra and geometry. In this paper we present a method which intermingles CAD construction with truth evaluation so that parts of the CAD are constructed only as needed to further truth evaluation and aborts CAD construction as soon as no more truth evaluation is needed. The truth evaluation utilizes in an essential way any quantifiers which are present and additionally takes account of atomic formulas from which some variables are absent. Preliminary observations show that the new method is always more efficient than the original, and often significantly more efficient”.

Reviewer: T.Pheidas (Iraklion)

##### MSC:

68W30 | Symbolic computation and algebraic computation |

##### Software:

QEPCAD
PDF
BibTeX
XML
Cite

\textit{G. E. Collins} and \textit{H. Hong}, J. Symb. Comput. 12, No. 3, 299--328 (1991; Zbl 0754.68063)

Full Text:
DOI

**OpenURL**

##### References:

[1] | Arnon, D.S., Algorithms for the geometry of semi-algebraic sets, (), Technical Report 436 |

[2] | Arnon, D.S., A cluster-based cylindrical algebraic decomposition algorithm, J. symbolic comp., 5, 1,2, 189-212, (1988) · Zbl 0648.68056 |

[3] | Arnon, D.S.; Collins, G.E.; McCallum, S., Cylindrical algebraic decomposition I: the basic algorithm, SIAM J. comp., 13, 865-877, (1984) · Zbl 0562.14001 |

[4] | Arnon, D.S.; Mignotte, M., On mechanical quantifier elimination for elementary algebra and geometry, J. symbolic comp., 5, 1,2, 237-260, (1988) · Zbl 0644.68051 |

[5] | Buchberger, B.; Collins, G.E.; Kutzler, B., Algebraic methods for geometric reasoning, (1989), Manuscript in preparation |

[6] | Collins, G.E., Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition, (), 134-183 |

[7] | Collins, G.E.; Hong, H., Computing coarsest squarefree bases and multiplicities, () |

[8] | Collins, G.E.; Johnson, J., Quantifier elimination and the sign variation method for real root isolation, (), 264-271 |

[9] | Collins, G.E.; Loos, R., The ALDES-SAC2 computer algebra system, Technical report, (1980) |

[10] | Davenport, J.H.; Heintz, J., Real quantifier elimination is doubly exponential, J. symbolic comp., 5, 1,2, (1988) · Zbl 0663.03015 |

[11] | Hong, H., An improvement of the projection operator in cylindrical algebraic decomposition, (), 261-264 |

[12] | Hong, H., Improvements in CAD-based quantifier elimination, () |

[13] | Hong, H., Collision problems by an improved CAD-based quantifier elimination algorithm, () |

[14] | Hong, H.; Kuechlin, W., Termination proof of term rewrite system by cylindrical algebraic decomposition, (1990), Manuscript in preparation |

[15] | Huet, G.; Oppen, D., Equations and rewrite rules, (), 349-405 |

[16] | Lankford, D.S., On proving term rewriting systems are Noetherian, () |

[17] | Loos, R., Computing in algebraic extensions, (), 173-188 · Zbl 0576.12001 |

[18] | McCallum, S., An improved projection operator for cylindrical algebraic decomposition, () · Zbl 0900.68279 |

[19] | McCallum, S., Solving polynomial strict inequalities using cylindrical algebraic decomposition, () · Zbl 0789.68080 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.