On propagation of equational constraints in CAD-based quantifier elimination | Macquarie University ResearchOnline

Home

Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.14/16245

27 Visitors

32 Hits

0 Downloads

Title: On propagation of equational constraints in CAD-based quantifier elimination
Related: Twenty-Sixth International Symposium on Symbolic and Algebraic Computation (22-25 July 2001 : Ontario, Canada)
Related: Proceedings of the 26th International Symposium on Symbolic and Algebraic Computation
DOI: 10.1145/384101.384132
Publisher: New York : ACM Press
Date: 2001
Author/Creator: McCallum, Scott
Description: 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 follows on from [11], and validates the use of a semi-restricted equational projection scheme throughout the projection phase of cad. The fully restricted projection scheme as originally proposed in [4] is proved valid for four variable problems under certain conditions.
Description: 8 page(s)
Subject Keyword: performance
Subject Keyword: reliability
Subject Keyword: theory
Subject Keyword: verification
Resource Type: conference paper
Organisation: Macquarie University. Dept. of Computing

Macquarie University ResearchOnline