On projection in CAD-based quantifier elimination with equational constraint

S McCallum*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

Abstract

Collins [4] observed that quantifier elimination problems often have equational constraints, and he asserted that such constraints can be used to reduce the projection sets required for cylindrical algebraic decomposition (cad) based quantifier elimination. This paper provides a detailed partial validity proof for the restricted equational projection method outlined by Collins [4]. The proof is sufficient to validate the use of the method for the first projection of the projection phase. 4 further consequence is that the method can be used for both the first and second projections in the case of a trivariate quantifier elimination problem having sufficient equational constraints.

Original languageEnglish
Title of host publicationISSAC 99: PROCEEDINGS OF THE 1999 INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION
EditorsS Dooley
Place of PublicationNew York, NY
PublisherASSOC COMPUTING MACHINERY
Pages145-149
Number of pages5
ISBN (Print)1581130732
DOIs
Publication statusPublished - 1999
EventInternational Symposium on Symbolic and Algebraic Computation - VANCOUVER, Canada
Duration: 29 Jul 199931 Jul 1999

Conference

ConferenceInternational Symposium on Symbolic and Algebraic Computation
CountryCanada
CityVANCOUVER
Period29/07/9931/07/99

Keywords

  • CYLINDRICAL ALGEBRAIC DECOMPOSITION

Cite this