On projection in CAD-based quantifier elimination with equational constraint

S McCallum

doi:10.1145/309831.309892

On projection in CAD-based quantifier elimination with equational constraint

S McCallum^*

^*Corresponding author for this work

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

68 Citations (Scopus)

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 language	English
Title of host publication	ISSAC 99: PROCEEDINGS OF THE 1999 INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION
Editors	S Dooley
Place of Publication	New York, NY
Publisher	ASSOC COMPUTING MACHINERY
Pages	145-149
Number of pages	5
ISBN (Print)	1581130732
DOIs	https://doi.org/10.1145/309831.309892
Publication status	Published - 1999
Event	International Symposium on Symbolic and Algebraic Computation - VANCOUVER, Canada Duration: 29 Jul 1999 → 31 Jul 1999

Conference

Conference	International Symposium on Symbolic and Algebraic Computation
Country/Territory	Canada
City	VANCOUVER
Period	29/07/99 → 31/07/99

Keywords

CYLINDRICAL ALGEBRAIC DECOMPOSITION

Access to Document

10.1145/309831.309892

Cite this

@inproceedings{2e172e4b6adb4821b986862d47f41ec2,

title = "On projection in CAD-based quantifier elimination with equational constraint",

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.",

keywords = "CYLINDRICAL ALGEBRAIC DECOMPOSITION",

author = "S McCallum",

year = "1999",

doi = "10.1145/309831.309892",

language = "English",

isbn = "1581130732",

pages = "145--149",

editor = "S Dooley",

booktitle = "ISSAC 99: PROCEEDINGS OF THE 1999 INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION",

publisher = "ASSOC COMPUTING MACHINERY",

note = "International Symposium on Symbolic and Algebraic Computation ; Conference date: 29-07-1999 Through 31-07-1999",

}

McCallum, S 1999, On projection in CAD-based quantifier elimination with equational constraint. in S Dooley (ed.), ISSAC 99: PROCEEDINGS OF THE 1999 INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION. ASSOC COMPUTING MACHINERY, New York, NY, pp. 145-149, International Symposium on Symbolic and Algebraic Computation, VANCOUVER, Canada, 29/07/99. https://doi.org/10.1145/309831.309892

On projection in CAD-based quantifier elimination with equational constraint. / McCallum, S.
ISSAC 99: PROCEEDINGS OF THE 1999 INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION. ed. / S Dooley. New York, NY: ASSOC COMPUTING MACHINERY, 1999. p. 145-149.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - On projection in CAD-based quantifier elimination with equational constraint

AU - McCallum, S

PY - 1999

Y1 - 1999

N2 - 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.

AB - 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.

KW - CYLINDRICAL ALGEBRAIC DECOMPOSITION

U2 - 10.1145/309831.309892

DO - 10.1145/309831.309892

M3 - Conference proceeding contribution

SN - 1581130732

SP - 145

EP - 149

BT - ISSAC 99: PROCEEDINGS OF THE 1999 INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION

A2 - Dooley, S

PB - ASSOC COMPUTING MACHINERY

CY - New York, NY

T2 - International Symposium on Symbolic and Algebraic Computation

Y2 - 29 July 1999 through 31 July 1999

ER -

On projection in CAD-based quantifier elimination with equational constraint

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this