Article

Free access

On projection in CAD-based quantifier elimination with equational constraint

Author:

Scott McCallumAuthors Info & Claims

ISSAC '99: Proceedings of the 1999 international symposium on Symbolic and algebraic computation

Pages 145 - 149

https://doi.org/10.1145/309831.309892

Published: 01 July 1999 Publication History

PDF eReader

References

[1]

ABIIYANK-X{t. S. S. Algebraic Geometry for Scie.ntist~ and Engineers. American Mathcinatical Society. Providence, 1990.

Google Scholar

[2]

ARNON, D. S. C, OI,I,INS. G. E., AND h,"{CC.AI.I,UM, S. Cylindrical algebraic decomposition i" The J)asic algorithm. SIAM,lournal on Computing 13 (1984), 865- 877.

Digital Library

Google Scholar

[3]

COt~I~INS, G. E. Quantifier elimi,mtion h~r real closed fields by cylindri(:al algebraic de(:or,~posit.io,~. In Proceedings of 2nd GI Conference on Automata Theory and ForTr~al Languages, Lecture Notes in Computer Scie.nc.e 33 (Berlin, 1975), Springer-Verlag, pp. 134-1.83.

Crossref

Google Scholar

[4]

COLLINS, G. E. Quantifier elimination 1)y cylindrical algebraic decomt,osit.ion twenty years of progress, hi Quant,ifier Eliminatiov, and Cylindrical Algebraic Decor,.position (Vienna, 1998), B. F. Caviness and J. R. Johnson, Eds., Springer-Verlag, pp. 8-23.

Google Scholar

[5]

C',OI.I:INS, G. E., ANJ~ HONG, H. Partial cylindrical ~lgebraic decomposition fbr quantifier elimination. Journal of Symbolic Computation .1~ (1991), 299 328.

Digital Library

Google Scholar

[6]

I~AI'LAN. W. Introduction to Analytic Functions. Addison-Wesley, Reading, 1966.

Google Scholar

[7]

MCC:AI~I~IJM, S. An ImpTvved Projection Operation for Cylindrical Alg~braic Decomposition. PhD thesis, University of Wisconsin-Madison, 1984.

Google Scholar

[8]

MCCALLUM. S. An improved projection operation for cylindric,~l algebraic decomposition of threedimensional space.,lournal of Symbolic Computation 5 (1988), 141-161.

Digital Library

Google Scholar

[9]

MCC, AI~I~UM, S. An improved projection opcrat, ion tbr cylindrical algebraic decomposition. In Quant4fier Elimination and Cylindrical Algebraic Decomposition (Vienna, 1998), B. F. Caviness and J. R. Johnson, Eds., Springer-Verlag, pp. 242-268.

Google Scholar

[10]

\~AI.KEr~. R. J. Algebraic Curves. Springer-Verlag, N(;w

Google Scholar

[11]

\~'HITNE'~, H. Complex Analytic Varieties. Addisoil- Wesley, Menlo Park, 1972.

Google Scholar

Cited By

View all

Huang BWang DYang J(2024)Jacobi Stability Analysis for Systems of ODEs Using Symbolic ComputationProceedings of the 2024 International Symposium on Symbolic and Algebraic Computation10.1145/3666000.3669689(180-187)Online publication date: 16-Jul-2024
https://dl.acm.org/doi/10.1145/3666000.3669689
Akshay SChakraborty SGoharshady AGovind RMotwani HVaranasi S(2024)Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticFormal Methods10.1007/978-3-031-71162-6_6(111-130)Online publication date: 11-Sep-2024
https://doi.org/10.1007/978-3-031-71162-6_6
Labahn GRiener CSafey El Din MSchost EVu T(2023)Faster real root decision algorithm for symmetric polynomialsProceedings of the 2023 International Symposium on Symbolic and Algebraic Computation10.1145/3597066.3597097(452-460)Online publication date: 24-Jul-2023
https://dl.acm.org/doi/10.1145/3597066.3597097
Show More Cited By

Index Terms

On projection in CAD-based quantifier elimination with equational constraint

Recommendations

On propagation of equational constraints in CAD-based quantifier elimination
ISSAC '01: Proceedings of the 2001 international symposium on Symbolic and algebraic computation

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 ...
Second Order Quantifier Elimination: Foundations, Computational Aspects and Applications
Negation Elimination from Simple Equational Formulae
ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming

Equational formulae are first-order formulae over an alphabet F of function symbols whose only predicate symbol is syntactic equality. Unification problems are an important special case of equational formulae, where no universal quantifiers and no ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ISSAC '99: Proceedings of the 1999 international symposium on Symbolic and algebraic computation

July 1999

314 pages

ISBN:1581130732

DOI:10.1145/309831

Chairmen:
Keith Geddes
Univ. of Waterloo, Waterloo, Ont., Canada
,
Bruno Salvy
INRIA Rocquencourt, France
,
Editor:
Sam Dooley
IBM Research, Yorktown Heights, NY

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ISSAC99

Sponsor:

ISSAC99: International Symposium on Symbolic and Algebraic Computation

July 28 - 31, 1999

British Columbia, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 395 of 838 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

54
Total Citations
View Citations
398
Total Downloads

Downloads (Last 12 months)58
Downloads (Last 6 weeks)11

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Huang BWang DYang J(2024)Jacobi Stability Analysis for Systems of ODEs Using Symbolic ComputationProceedings of the 2024 International Symposium on Symbolic and Algebraic Computation10.1145/3666000.3669689(180-187)Online publication date: 16-Jul-2024
https://dl.acm.org/doi/10.1145/3666000.3669689
Akshay SChakraborty SGoharshady AGovind RMotwani HVaranasi S(2024)Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticFormal Methods10.1007/978-3-031-71162-6_6(111-130)Online publication date: 11-Sep-2024
https://doi.org/10.1007/978-3-031-71162-6_6
Labahn GRiener CSafey El Din MSchost EVu T(2023)Faster real root decision algorithm for symmetric polynomialsProceedings of the 2023 International Symposium on Symbolic and Algebraic Computation10.1145/3597066.3597097(452-460)Online publication date: 24-Jul-2023
https://dl.acm.org/doi/10.1145/3597066.3597097
Davenport JNair ASankaran GUncu A(2023)Lazard-style CAD and Equational ConstraintsProceedings of the 2023 International Symposium on Symbolic and Algebraic Computation10.1145/3597066.3597090(218-226)Online publication date: 24-Jul-2023
https://dl.acm.org/doi/10.1145/3597066.3597090
Nalbach JÁbrahám ESpecht PBrown CDavenport JEngland M(2023)Levelwise construction of a single cylindrical algebraic cellJournal of Symbolic Computation10.1016/j.jsc.2023.102288(102288)Online publication date: Dec-2023
https://doi.org/10.1016/j.jsc.2023.102288
Bradford RDavenport JEngland MSadeghimanesh AUncu A(2022)The DEWCAD projectACM Communications in Computer Algebra10.1145/3511528.351153855:3(107-111)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3511528.3511538
McCallum SNair ADavenport JSankaran G(2020)The CAD Conundrum: Lex-Least vs Order2020 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)10.1109/SYNASC51798.2020.00017(32-35)Online publication date: Sep-2020
https://doi.org/10.1109/SYNASC51798.2020.00017
England MBradford RDavenport J(2020)Cylindrical algebraic decomposition with equational constraintsJournal of Symbolic Computation10.1016/j.jsc.2019.07.019100:C(38-71)Online publication date: 1-Sep-2020
https://dl.acm.org/doi/10.1016/j.jsc.2019.07.019
Ábrahám EDavenport JEngland MKremer G(2020)Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coveringsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2020.100633(100633)Online publication date: Nov-2020
https://doi.org/10.1016/j.jlamp.2020.100633
Brown CMcCallum S(2020)Enhancements to Lazard’s Method for Cylindrical Algebraic DecompositionComputer Algebra in Scientific Computing10.1007/978-3-030-60026-6_8(129-149)Online publication date: 2-Oct-2020
https://doi.org/10.1007/978-3-030-60026-6_8
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

On propagation of equational constraints in CAD-based quantifier elimination

Second Order Quantifier Elimination: Foundations, Computational Aspects and Applications

Negation Elimination from Simple Equational Formulae